Correct Blockchain-based Business Processes

Apr 5 11:00 ₂₀₂₂

Abstract: A business process is a chain of events, activities, and decisions intended to achieve a specific organizational goal. Business Process Management (BPM) is a systematic approach to improving these processes.

Blockchain refers to an emerging distributed database technology that relies on a tamper-proof list of timestamped transaction records. Particular attention is paid to the integration of this technology into business processes. This integration makes it possible to create intelligent business processes. In fact, several blockchains are used in several areas, such as cryptocurrency transactions, authenticity, and storage. They provide a way to run processes reliably even in a network without any mutual trust between its nodes. One of the most interesting concepts in blockchain technology is that of smart contracts. A smart contract can be used in the definition of collaborative business processes in general and inter-organizational in particular.

The integration of blockchain technology and business processes still faces complex issues. We are particularly interested in the problem of verifying the correctness of blockchain-based business processes.

We started with a study of the state of the art of the two main areas of research underlying our subject, namely Blockchain technology and Business Process Management. Particular attention has been paid, on the one hand to studies that have begun to explore the possibilities of using Blockchain in the context of BPM, and on the other hand to studies that have touched on the subject of verification of smart contracts in general. Having decided to focus on the formal verification of smart contracts, we have proposed a formal approach based on the transformation of Solidity smart contracts, with consideration of the BPM context in which they are used, into a Hierarchical Coloured Petri net. We express a set of smart contract vulnerabilities as temporal logic formulae and use the Helena model checker to, not only detect such vulnerabilities while discerning their exploitability, but also check other temporal-based contract-specific properties. Our proposed approach is based on model checking of CPN models and comprises mainly three phases:

• transforming the smart contracts' Solidity code into CPN submodels corresponding to their functions.
• transforming the BPM context into a CPN model
• constructing a CPN model w.r.t an LTL property that can express: (i) a vulnerability in the code or (ii) a contract-specific property, linking it to a CPN model representing the behavior to be considered, and feeding it the model checker to verify the targeted property.

More precisely, we opt for a hierarchical CPN to represent the considered smart contracts' execution and interaction w.r.t the provided BPM context specification.

We have implemented a graphical tool called Solidity2CPN that automates the different steps of the proposed approach and makes it accessible to a broader range of users who are unfamiliar with the aspects of formal verification.

Keywords: Blockchain, Business Process Management, Model Checking, Solidity, Smart Contracts, Hierarchical Coloured Petri Nets \and Temporal properties.