Formal verification of Reentrancy Vulnerability Based on CPN

doi:10.21203/rs.3.rs-1997012/v1

Download PDF

Research Article

Formal verification of Reentrancy Vulnerability Based on CPN

https://doi.org/10.21203/rs.3.rs-1997012/v1

This work is licensed under a CC BY 4.0 License

Version 1

posted

You are reading this latest preprint version

A smart contract is a special form of computer program running on a blockchain, which provides a new way to implement financial and business transactions in a free-of-conflicts and transparent environment. In blockchain systems, such as Ethereum, smart contracts can handle and autonomously transfer assets of considerable value to other parties. Hence, it is particularly important to ensure that smart contracts function as intended since bugs or vulnerabilities may lead and indeed have led, to substantial economic losses and erosion of trust for blockchain. While a number of approaches and tools have been developed to find vulnerabilities, formal method presents the highest level of confidence about the security of smart contracts. In this paper, we propose a formal solution to model smart contract based on Colored Petri Net (CPN). Herein we focus on the most common type of security bugs in smart contract, i.e., reentrancy bug, which led to a serious financial loss of around $60 million in 2016. We present a hierarchical CPN modelling method to analyze potential security vulnerabilities at the contract’s source code level. Then modeling analysis methods such as correlation matrix, state space report and state space graph generated by CPN Tools simulation were exploited for formal analysis of smart contracts. The example shows the full state space and wrong path in accordance with our expected results. Finally, the conclusion was verified in the Ethereum network based on Remix platform.

smart contract

CPN

reentrancy vulnerability

Petri net

Since the introduction of Bitcoin in 2009 [Nakamoto S, 2018]，the first decentralized cryptocurrency has gained considerable attention and adoption. As of 2022, there are approximately 20,457 cryptocurrencies that can be tracked by CoinMarketCap. A cryptocurrency is administrated by distributed network nodes without involving a trusted third party or central agency. The nodes share and secure a public and append-only ledger of transactions, i.e., blockchain. In recent years, the popular Ethereum [Buterin, 2014] blockchain started the era of Blockchain 2.0 by introducing Turing-complete smart contract, with a wide range of applications including auctions [Blass, 2018], elections [Zou, 2019], crowdfunding, and cross-industry finance far beyond cryptocurrency [Wang, 2019].

Currently, tens of thousands of transactions are processed on Ethereum (the most famous smart contract platform) every day since its launch in July 2015, whose capitalization has reached more 100 billion as by July 2022. As such, we only consider smart contracts on Ethereum blockchain in this work.

The term “smart contract” was first proposed in 1990s by computer scientist and cryptographer Nick Szabo [Szabo, 1997], who defined a smart contract as “a set of commitments, specified in the digital form, including protocols of the contract participants [Szabo, 1996].” But due to the lack of trusted environment, smart contract did not receive widespread attention and research at that time. The emergence of blockchain technology has redefined and made possible smart contracts. In the context of blockchain, a smart contract is a self-executing computer program that running on blockchain. It will automatically execute any task when predefined conditions are met.

The security of smart contracts has become a major concern for the healthy development of Ethereum. A smart contract in the blockchain often carry financial values worthy of millions of dollars. Holding so much wealth, however, making smart contracts lucrative and profitable targets for malicious attackers. [Liu, 2019]. A bug, flaw or error in a smart contract may produce an unexpected result or behave in unintended ways, resulting in devastating consequences. For instance, by exploiting the reentrancy vulnerability in the DAO [Mehar, 2019] smart contract’s source code, an attacker managed to drain more than $60 million worth of Ether in 2016. In addition, the SpankChiain contract [Usman, 2021] has also suffered reentrancy attack in 2018, which caused $40,000 stolen for lack of proper authority management. Similarly, in January 2020, the Uniswap [Wang, 2021] and Lendf.Me [Ferreira, 2021] projects were subject to the same reentrant bug again. It can be seen that a security vulnerability may cause irreparable losses to the project or investors. Reentrancy vulnerabilities are one of the most serious vulnerabilities in smart contracts, which are discovered and exploited from time to time, undermining the trust for smart contract-based applications [Liu, 2021].

Traditional informal analysis method mainly focuses on the analysis of logic control behavior, which is no longer enough to deal with the complex and changeable on-chain data state environment. Whereas the formal verification method is based on mathematical models and reasoning, which is more rigorous and reliable. In recent years, the formal method has received more and more attention in the security verification of smart contracts. In this paper, we conduct a formal analysis method based on CPN [Gehlot, 2010], and strives to analyze and verify the reentrancy vulnerabilities of smart contracts from different perspectives. We choose this formalism because of its ability to combine the strong description ability of Petri nets with the expressive power of programming languages. In order to describe TheDAO contract more accurately, concepts such as data attributes, key data elements, and key transitions are added, and the smart contract is described from the perspective of data flow and control flow, in which the data state reflects the change of the transaction state, and the control flow reflects some key operations during transaction process. Then, we utilize modeling tools in CPN to model the simplified TheDAO contract hierarchically, including the whole contract, non-attack operation and attack operation respectively, which avoid the loss of context-based information and the influence of under-approximation Furthermore, adopt the simulation tools in CPN to shows the specific execution process of contract. The results not only discover the logic loopholes at the Solidity language level, but also find the malicious attack behavior against custom specifications of contacts in real life. Also, uses the state analysis method to analyze the model, and obtains an executable attack transition sequence. Finally, the correctness of the conclusion is confirmed on the Remix platform.

The remainder of this paper is structures as follows. Section 2 provides essential background knowledge of smart contracts. Section 3 describes the property specification and model building of The DAO. In section, we conduct experimental analysis from many aspects and verify our results based on the Remix platform. Section 5 discussed the related work about reentrancy vulnerability detection. Finally, we conclude this paper and future work in Section 6.

In this section, we introduce background knowledge about smart contract, Colored Petri net as well as The DAO contract.

2.1 Ethereum and smart contract

There are many blockchain platforms supporting the operation of smart contracts, such as EOS, BCOS, Fabric, CITA, etc. Among them, Ethereum is the largest, oldest and most influential one [Tolmach, 2021]. It uses Solidity [Pierro, 2020] programming language to develop smart contracts and provides a large number of application program interfaces (APIs). The deployment of the contract is realized by sending a transaction to the blockchain. The receiver of the transaction is empty and contains bytecode and other information. After the miner successfully packages the transaction, an address is returned. This address is the contract address, and the invocation or access of the contract needs to go through this address, which is the unique identifier of the contract. Smart contracts are compiled and interpreted and executed using Ethereum virtual machines (EVM) installed on each Ethereum node. Ethereum accounts fall into two categories: one is external accounts, which invoke contracts by sending transactions call. Transactions are broadcast to all nodes of the Ethereum network, packaged and verified by miners, and all transaction records are stored in the blockchain. The other is an internal account that calls other contracts through message calls. The message is transfer of internal parameters and will not synchronized to the blockchain. Therefore, the contract invoked by message invocation between contracts will not be recorded in the chain.

2.2 Features of Smart contracts

A couple of reasons could account for that why smart contracts are particularly prone to errors. Compared with ordinary programs, smart contracts have many different features. Ethereum smart contracts run on the blockchain, and their complete lifecycle includes development, compilation, deployment, invocation, and destruction, many of which are triggered by Ethereum transactions with the flow of assets between contract participants. Hence, smart contract programming requires an “economic thinking” perspective, which is undoubtedly a challenging task for traditional programmers. [Schneidewind, 2020] In addition, smart contract programs also have special mechanisms such as gas restrictions, delegated calls, and code that cannot be modified updated or fixed due to the immutability of blockchains. These differences bring new security risks and attack surfaces to smart contracts, practitioners are required to take into consideration all possible situation and environments may encounter in the future. As a result, a rigorous security analysis of smart contracts is of great significance before deployment.

2.3 Colored Petri Net

Petri net is a formal model for modeling discrete event concurrent systems, which was proposed by German scholar Carl Adam Petri in 1960s. It can not only describe the structure of the system, but also simulate the operation of the system. Petri includes two types of nodes, place and transition, and adds a token distribution representing state information to the set of places. Places and transitions are connected by directed arcs, and the tokens in the place represent the resources or data that can be used. Despite the advantages of concurrency and synchronization, Petri has the problem of space explosion. Colored Petri nets (CPN) was founded in 1981 by Professor Jensen [Ma, 2018] in order to overcome the bottleneck problem of Petri nets. On the basis of Petri net, the problem scale of basic Petri net is simplified by adding color set and variable definition, which greatly complements the abstraction and description ability of Petri net. The built-in mechanism of CPN includes hierarchical structure, fusion set, entity folding, etc., reducing the possibility of state space explosion. CPN Tools is a modeling tool for editing, simulating and analyzing colored Petri nets. Using CPN Tools, it is possible to study the behavior of the modeled system by means of simulation, and generate state-space reports. The generated state space directed graph can not only precisely locate the wrong path, but also display the status of each node in the path, which is convenient for analyzing the cause and improving the contract code. The formal definition of CPN is given as follows.

2.4 The DAO Smart Contract

TheDAO (Decentralized Autonomous Organization) is an open source project of the German startup Slock.it, which raises money through Ethereum and lock it into a smart contract. Then each investor participating in the crowdfunding will obtain the corresponding DAO token as shares according to the amount of investment, and jointly decide the invested project through voting, and the entire community is fully autonomous. TheDAO completed the crowdfunding on May 28, 2016, raising a total of 11.5 million ETH worth of $149 million at the time, which is by far the largest crowdfunding project. The part code of the token exchange contract is shown in Fig. 1. The contract owner can deposit and withdraw normally by calling the deposit () function in line 2 and withdraw () function in line 5.

But the DAO experiment failed soon after it was launched, when hackers exploited a vulnerability in the recursive calls in TheDAO smart contract (i.e., a re-entry vulnerability) to attack it, resulting in the hijacking of $60 million worth of Ether. As shown in Fig. 2, the attacker leverages the call.value in line 8 of the code that contains the default fallback function to carefully construct the code for the attack. The logic defect of the contract lies in that the ether are sent to the attacker's address first, and then the DAO balance of the attacker's account is reduced or cleared accordingly. Therefore, before clearing the balance, the attacker can exchange a large amount of ether with a small amount of DAO coins by constantly calling the fallback function. This not only brought huge losses to the crowdfunding participants, but also caused the first hard fork in the history of Ethereum, which attracted widespread concern in the industry.

The essence of reentrancy is that due to the participation of attack behavior, the data state of the entire transaction process is inconsistent, violating the relevant properties of the transaction, such as transaction integrity and fund consistency. Therefore, we exploit set D to describe the data elements used in the transaction process. It is also a collection of token types. For some data elements that play a key role in the attack process like user’s contract balance, public wallet balance, etc., a key token type is established in the model, which is recorded as S. Predicates are assigned to transitions that characterize validation conditions in a transaction.

In this section, we establish the property specification according to the simplified TheDAO contract, and exploit CPN Tools to conduct top-down hierarchical modeling, including the overall model and attack-free model, as well as the attacker model based on the transaction attack behavior.

3.1 Attribute specifications

By analyzing the contents of the contract, it is stipulated that the contract needs to meet the following conventions.

Investors must ensure sufficient ether when exchanging ether for DAO tokens, and can withdraw at any time without affecting the operation of the contract;
Investors can only perform one of the two operations of deposit (Ether to DAO coin) or withdraw (DAO coin to Ether) at a time;
When investors apply for deposit and withdrawal, the two balances of investors and the public wallet of crowdfunding should be updated in real time;
When the DAO coin balance in the investor's contract account is insufficient, the investor cannot apply to use the DAO coin to exchange ether;
Before and after the investor conducts any transaction, the investor's DAO coin balance and the sum of the ether balance after conversion should be consistent.

If TheDAO satisfies the above stipulation conditions during the execution process, it proves that the contract is safe.

3.2 Top-lever model

In order to describe the execution process of the overall model and explain the related results, we list the relevant definitions in Table 1.

Table 1

CPN Model Definitions
Type	Annotation
P[place]	Refer to input data flow places
T[transition]	Refer to input control flow transitions
CS[colerset]	Refer to“colerset”as 名称
IM[place]	Initial place value
M[place]	Local place marking value
ARC[node₁,node₂]	Binded transmission value on the arc, node₁,node₂ as input and output node

Based on CPN Tools, the top-level model of TheDAO is shown in Fig. 3, which includes 3 places and 2 alternative transitions. It should be noted that the conversion between Ether and DAO coins is not considered in the model construction process, and only simple The numbers are blurred to represent Ether and DAO coins.

In Fig. 3, Account represents the investor account involved in crowdfunding, Bank represents the investor contract account, and Cfd represents the total contract account of crowdfunding project.

T[Deposit] and T[WithDraw] both are substitution transition, which represents the deposit operation and withdrawal operation respectively. IM[Account]={account = 6}, IM[Bank]={bank = 0}, IM[Cfd]={Cfd = 25}.

3.3 Attack-free Model

The model without attack is shown in Figs. 4 and 5. They are the lower implementations of the top-level model that replace the transitions deposit and withdraw. In the Deposit layer, the model contains 8 places and 3 transitions, while in the WithDraw layer, it contains 14 banks and 3 transitions. The relevant information of data stored by nodes in Fig. 4 of the underlying model is explained as follows. The names of transitions and places in Fig. 5 are similar to those in Table 2. To save space, we will not explain them one by one here.

Table 2

Part Nodes Definitions
Type	Annotation
P[Account]	Investor Account
P[Gas _Need]	Consumed gas
P[Deposit_To]	Plan to deposit balance
P[deposit]	Deposit balance
P[Old_bal0]	Investor account origial balance
P[Bank]	Investor account balance
P[Cfd]:	Crowdfunding balance

In CPN Tools, we assign initial values to the model, such that P[Account]:1`6、P[Bank]:1`0、P[Cfd]:1`25, i.e. IM[Account]={account = 6}, IM[Bank]={bank = 0}, IM[Cfd]={Cfd = 25}, IM[Gas_Need] ={gas = 1}. Since the data in the place is single, it can be abbreviated as IM[Account] = 6, IM[Bank] = 0, IM[Cfd] = 25. which are similar below. From the initial value, we observe the execution process of the DAO model without attack. The state sequence in the running process of the model is represented by S_n(n = 1,2,3…).Firstly, the running process of Deposit layer of simulation model is as follows.

① S₁[Start > S₂.

ARC < Account,Start>={userbal = 6},T[Start] is enabled. The investor sends a transaction request, and the state of the model changes from S₁ to S₂ after T[Start] occurs, and M[Old_bal] = 6, M[Account] = 0.

② S₂[D_Judge > S₃.

ARC < Old_bal,D_judge>={userbal = 10},ARC < Gas_Need,D_judge>={g = 1},ARC < Deposit_To, D_Judge> ={deposit = 4}, T[D_judge] is fired. Now the state of the model is transformed from S₂ to S₃. Then, M[deposit] = 5,M[Old_bal0] = 6,M[Gas_Need] = 1,M[Deposit_To] = 5, M[Old_bal] = 0.

③ S₃[Deposit > S₄.

ARC < deposit,Deposit>={m = 5}, ARC < Old_bal0,Deposit>={userball = 6}, ARC < Bank,Deposit>={b = 0}, ARC < Cfd,Deposit>={c = 25}. T[Deposit] is enabled. At this time, M[Account] = 1,M[Bank] is binded to 5 and M[Cfd] = 30. After that, no transition can be triggered and the model finishes running.

Next, the WithDarw layer is executed by the simulation tool, and the initial state of the model is IM[Account] = 6, IM[Bank] = 0, IM[Cfd] = 25, IM[T_Gas] = 1. The execution process is as follows.

① S₁[Sart > S₅.

ARC < Account,Sart>={account = 6},T[Take] is fired. The investor sends a transaction request, and the state of the model changes from S₁ to S₅, and M[Old_bal1] = 10.

② S₅[T_Judge > S₆.

ARC < Old_bal1,T_judge>={oldbal = 1},ARC < T_Gas,T_judge>={g = 1},ARC < T_Take,T_Judge>={m = 4}, ARC < Bank,T_Judge>={b = 5}, ARC < Cfd,T_Judge>={c = 25}. When the transition condition is satisfied, T[D_judge] is triggered to fire, and the state of the model is converted from S₅ to S₆. At this time, M[T_Gas] = 1,M[T_Take] = 5.M[T_Old] = 1,M[T_bank] = 5,M[T_take],M[T_cft] = 30.

③ S₆[Fallback > S₇.

ARC < T_Old,Fallback>={oldbal = 1},ARC < T_bank,Fallback>={b = 5},ARC < T_Take,Fallback>={m = 5}, ARC < T_cft, Fallback >={c = 30}. T[Fallback] is enabled, then the state changes fromS₇ to S₈. In addition,M[T_Old0] = 1,M[T_bank0] = 5,M[T_Take0] = 5,M[T_cft0] = 30.

④ S₇[withdraw > S₈.

ARC < T_Old0,withdraw>={oldbal = 1},ARC < T_bank0, withdraw >={b = 5},ARC < T_Take0, withdraw>={m = 5}, ARC < T_cft0, withdraw>={c = 25}. At this point, T[withdraw] is triggered and the model state is converted from S₈ to S₉. M[Account] is bound to 6,M[Bank] is bound to 0 and M[Cfd] is bound to 25.At this time, the currency withdrawal operation is normal, and the model operation runs to completion..

3.4 Attacker Model

Since the attack mainly targets the WithDraw layer, we simulate the attacker's behavior to model the attack in Section 3.4, which is used to analyze whether the model can have reentrant vulnerabilities. Figure 6 shows the attack layer. Based on the WithDraw layer model above, the behavior of the attacker is added to the WithDraw layer of the original model (Fig. 5). Given the concurrency of the Petri net model, by adding the suppression arc and the place P[Hacker], we only consider the execution of the model after adding the Attack entity transition. The obtained one is the WithDraw layer of the attack model (Fig. 7). The attack layer model is merged with the new WithDraw layer to form theDAO attack model. When the initial state value is assigned, the malicious trading behavior of the attacker can be simulated. In the simulation tool, the initial state of the contract is as follows.

P[Account]:1`6
P[Bank]:1`0
P[Cfd]:1`25
P[Gas_Need]: 1`1
P[Deposit_To]:1`5
P[T_Gas]:1`1
P[T_Take]:1`5

The attack process of the new model is simulated as follows.

① S₆[Attack > S₇'

ARC < T_Old, Attack>={oldbal = 1},ARC < T_bank, Attack >={b = 5},ARC < T_Take, Attack >={m = 5}, ARC < T_cft, Attack >={c = 30}. At this point, T[Attack] is fired, and and the state of the model is changed from S₆ to S₇'. The Attack transition is set to be executed twice to simplify simulation execution. M[Account] is binded to 11 and M[T_Cfd] to 20.

② S₇' [withdraw > S₈'

When the number of attacks is reduced to 0, the contract returns to WithDarw layer for normal operation. At this time, T[withdraw] is executed, and M[Account] is finally updated to 16,M[Bank] = 0,M[Cft] = 15.

4.1 Non-secure state reachability analysis

The principle of matrix-based reachability analysis is to establish corresponding correlation matrix. Given the vector M₀ of the initial state and the unsafe state of CPN represented by a non-negative integer vector M, which are then substituted into the state equation to solve. If there is no solution, it means that the state is safe. On the contrary, if there is a solution, it means that there is a security loophole in the contract, and the sequence of attack transitions is given.

The association matrix of CPN model is shown in Table 1, Table 2 and Table 3, which are the submatrix M1 Deposit layer, submatrix M2 of WithDraw layer and submatrix of M3 Attack layer about the contract association matrix, respectively.

The initial state of the contract is M₀ = [0, Gas, Money, 0,0, Money, Money, Money,0,Gas,Take,0,0,…,0]. We assume that the unsafe state is M=[0, Gas,Money,0,0,0,..., Hacker,Attack_number,Money,Money,Money], indicating the data abnormality caused by the hacker's successful attack. M and M0 are substituted into the state equation M = M₀ + A^TX. To solve the state equation, t we can know that the equation has a solution by using the solution identification formula of linear function, and obtain an executable transition sequence: σ = T[Start] T[D_Judge] T[Deposit] T[Take] T[T_Judge] T[Attack] T[withdraw]. It can be concluded that the execution of the contract can reach this unsafe state, that is, there is at least one vulnerability in the smart contract, so that the attacker can exploit the vulnerability to steal illegal assets without hindrance.

4.2 CPN Tools State Space Analysis

In the fourth part above, we adopted the CPN Tools to model the whole Dao contract, non-attack operation and attack operation, respectively. By observing the results before and after the implementation of the model, we extracted the changes identified by Account, Bank and Cfd from the generated state space and summarized them, as shown in Table 4, Table 5 and Table 6.

Table 4

Account、Bank、Cfd Identification Change at Normal Deposit Operation Without Attack
Deposit layer	account	bank	Cfd
Before Execution After Execution	5 1	0 5	25 30

Table 5

Account、Bank、Cfd Identification Change at NormalWithDraw Operation Without Attack
WithDraw Layer	account	bank	Cfd
Before Execution After Execution	1 6	5 0	30 25

Table 6

Account、Bank、Cfd Identification Change With Attack
Attack Model	account	bank	Cfd
Before Execution During Execution After Execution	6 1 16	0 5 0	25 30 15

It can be seen from Table 4 and Table 5 that in the no-attack mode, the contract is executed normally, and all (1) ~ (4) of the property specification are satisfied. When the contract is attacked, the user performs deposit operations without any exception, but when the user performs withdrawal operations (Table 6), it can be found that the Account balance is 16 and the Cfd Account balance is 15. During the execution process, the malicious attacker not only withdraws the 5 Ether from the Account he deposited in the contract, but also steals an additional 10 Eth from the crowdfunded contract wallet. This shows that in the process of withdraw operation, the investor's balance, the investor's contract account balance, and the public wallet of the crowdfunding did not change in real time according to the attribute specification. Moreover, the sum of the investor's token balance and Ether balance is not consistent after any transaction by the investor. Attribute specifications (3) and (5) are violated. The contract is now in an insecure state.

4.3 CPN Tools status report analysis

Using CPN Tools to generate partial status reports of the non-attack model and the attacked model are shown in (a) and (b) of Fig. 8.

1. In the attack-free mode, all markings are home states, that is, starting from the current marking along any path, you can return to this marking, which denotes that the smart contract works well. At the same time, based on the SML language, ASK-CTL is used to verify whether the initial marking satisfies the home state property. The execution language and results are shown in Fig. 9. Among them, val it = true:bool means the judgment is true, i.e., the initial identifier is home state. In addition, it can be seen from Fig. 8(a) that the model without attack meets the activity without deadlock and dead transition, which show that all the identifiers in the model can generate the next identifier, and there is no unactivated transition. The contract specifications (1) ~ (5) are satisfied.

2. When there is an attack, it can be seen from 8(b) that identifier [52] is both a home state identifier and a dead identifier. This is because the appearance of malicious attackers makes Fallback become a dead transition. Based on the SML language, ASK-CTL was used to analyze the initial marking and the marking [52] respectively. According to the judgment result in Fig. 10, it can be seen that there is no dead transition in the attack model. The initial identification is no longer a home state, while the marking [52] is dead, which lead to abnormal data balance and the contract cannot operate continuously, thereby violating the property specification (1).

4.4 CPN Tools State diagram analysis

Based on the CPN Tools simulation tool, the state space is generated. Through observation, it can be seen that there are abnormal data transactions in the state space. Taking the user Account as an example, a series of abnormal transaction values such as 11, 16, 21, 26 appear in the data Account during the execution of the smart contract. Starting from the first marking M₁₀ of the value 11, we can trace a counter-example path, as shown in Fig. 11.According to the expanded state of marking M₉ and M₁₀, the balance in T’Old (i.e. Account account) has changed during the process from M₉ to M₁₀, while the Bank account balance is always 5.From this, we can determine that an exception has occurred, thus violating that the property specifications (3) and (5).And that the logical defect in the TheDAO contract can also been located from the location of the exception.

So far, a variety of methods have been used to analyze the model without attack and the model with attack, and the analysis results are consistent. That is to say, the smart contract has vulnerabilities that can be attacked, so that the attack can happen smoothly.

4.5 Conclusion Verification Based on the Remix Platform

In fact, as long as the number of attacks is enough, the attacker can transfer all the balance of the crowdfunding contract account. In order to confirm the correctness of the conclusion, experiments are carried out through the Remix platform. First use an account named (0xCA35b7d915458EF540aDe6068dFe2F44E8fa733c) is used to play the victim. Click the Deploy button to deploy the contract in Remix IDE, and deposit some ether. Here we put 25 ether into the contract wallet. At this time, we can find that the balance of the contract is 25Ether by clicking the wallet indicating that the deposit operation is successful, as shown in Fig. 12.

Next, we exploit another account (0x4B20993Bc481177ec7E8f571ceCaE8A9e22C02db) to act as an attacker, deploy the contract, and store 5Ether in the victim's wallet. At this time, we can see from Fig. 13 that the account of the victim's contract has become 30Ether.

The attacker calls the attack function to simulate an attack. Then call the wallet function of the attacked contract to check the balance of the contract, we can find that the balance is zero, which indicates 30ether in the attacked contract have been transferred to the attacker's contract. The result is shown in Fig. 14, which proves that the contract does have vulnerabilities that can be attacked. In addition, it also further shows that CPN modeling can correctly verify the potential reentrancy vulnerability of smart contracts.

In this section, we discuss the related work in the field of reentrancy vulnerabilities detection and formal verification of smart contract.

5.1 Reentracy Vulnerability Detection

Reguard [Liu, 2018] is a fuzzing-based analyzer for specially detecting reentrancy bus in Ethereum smart contract. Specifically, ReGuard consists of three key modules, namely, Contract Transformer, Fuzzing Engine and Core Detector. It parses the code of smart contracts into an intermediate representation, and then performs source-to-source transformation form IR to C++, which is realized in the contract transformer. The transformed C + + contracts remain the original behavior and interfaces to the well-designed fuzzing engine. As the fuzzing engine runs, Reguard executes a smart contract to identify reentrancy via runtime trace analysis, in which the trace is analyzed through Core Detector. A major challenge faced with fuzzing lies in that it tests programs in a random way [Feng, 2019]

Sereum [Rodler, 2018] is a novel design and implementation of smart contract security technology, which leverages the state updates of smart contract to detect malicious behavior without knowing the relevant semantic about the Solidity language. On the basis of existing Ethereum client, it extends to perform run-time monitoring by introducing taint engine and attack detector. The attack detector exploits taint engine to prevent suspicious state, which is said to the first applies taint-tracking solution to smart contracts. By running sereum on the massive Ethereum transactions, results demonstrate a high accuracy against attacks with little runtime overhead.

ReDetect [Yu, 2021] is a symbolic execution-based detection tool that targets reentrancy vulnerabilities of smart contract at the EVM bytecode level. Therefore, for Solidity-based contracts, it is necessary to compile the contract into EVM bytecode by means of compiler solc in the preprocessing phase. Then the EVM bytecode file is converted to EVM assembly code for constructing control flow graphs (CFG) with CFG Builder. After that, the proposed tool explores each possible path that may exist a reentrancy vulnerability and devises 5 path filters to reduce false positives.

Clairvoyance [Ye, 2020] is a cross-function and cross-contract static analysis for finding reentrancy vulnerabilities in smart contracts. It takes as input the source code (Solidity) of contracts, then builds cross-contract call graph and CFG to identify vulnerable call chains, which start with a suspicious contract address or object and end with a function call. By comparing Clairvoyance with three mainstream tools on 17,770 real contracts, which presents the best detection accuracy and proved to be an accurate and efficient detection method.

Reentrancy Analyzer (RA) [Chinen, 2020] is static analysis tool, which is a combination of symbolic execution and equivalence checking with the Z3 satisfiability modulo theories (SMT) solver to detect reentrancy attack within smart contracts. Analysts can implement the analysis of inter-contracts flows at EVM bytecode level without much prior knowledge about attacks in contracts. RA mainly verifies whether the program behavior with reentrancy attacks equals behavior on normal executions. The biggest advantage of tools is that this tool completely eliminates false positives and negatives.

Samreen et al. [Samreen, 2020] present a semi-automated framework targets reentrancy vulnerabilities in Ethereum smart contract, which combines static and dynamic analysis that detecting bug at runtime. In addition, deep learning technology has also been utilized for automatically discovering potential bugs. For example, et propose a sequential model [Qian, 2020], namely bidirectional long-short term memory with attention, for the precise detection task of reentrancy bugs, which promotes the future research interests in this field. Apart from the above vulnerability detection methods

5.2 Formal verification of smart contract

There are many methods of formal verification, among which theorem proving and model checking are the most widely used in the era of smart contracts. Bai et al. [Bai, 2018] proposed a formal verification framework. For an intelligent shopping scenario, Promel was utilized to model the intelligent shopping line, and SPIN was for testing the model, verifying the effect of formal methods on smart contracts. Qu et al. adopted the communication Sequence Process (CSP) theory to formally model concurrent programs [Qu, 2018], provided a framework for using CSP and FDR to check smart contract vulnerabilities, and successfully detected concurrent vulnerabilities in Ethereum public smart contracts. Amani et al. proposed a method for verifying Ethereum smart contracts at the EVM bytecode level [Amani, 2018] and extended the existing EVM formalization in Isabelle/HOL through sound program logic at the bytecode level. Sun et al. used formal methods to detect the security problems of smart contracts [Sun, 2020]. They summarized five types of security problems in smart contracts and proposed corresponding formal verification methods for each problem.

Kalra et al. proposed a framework called ZEUS [Kalra, 2018] to verify the correctness and fairness of smart contracts using abstract interpretation and symbolic model checking, as well as powerful constrained Horn clauses. Park et al. presented a formal verification tool UPPAAL [Park, 2018] to model and verify the Dutch auction trading system based on smart contracts, and set time constraints for each template and state in the modeling process. Dharanikota S et al. present CELESTIAL [Dharanikota, 2021], an open-source framework, allows programmers to translates the contracts and the specifications to F*, to formally verify real-world Ethereum smart contracts from different application domains. As a mature formal modeling method, Petri net is gradually applied to the behavior description and expression of smart contracts. Aiming at the satisfaction analysis of behavior attribute of smart contracts, Liu et al [Liu, 2019] models, analyzes and verifies the normal execution of smart contract and the process of attacking the contract by means of CPN Tools. DuoW et al. [Duo, 2020] introduced a formal analysis method of Ethereum smart contract based on CPN, which improved the existing bytecode program logic, defined more complete Hoare pre- and post-conditions, thereby making it suitable for the CPN modelling. Garfatta et al. (Garfatta, 2021) proposed a CPN-based formal verification method for Solidity smart contract. The main idea behind this approach is to transform the Solidity smart contracts to CPN. Then this model is analyzed and verified via checking temporal-based contract-specific properties. Thereafter, [Garfatta, 2022] continued to extend their work on mainly two aspects. One is taking the concept of function calls in the transformation into consideration. The other is to define the correctness properties of smart contracts as Linear Temporal Logic formalization.

With the popularization of blockchain platform-level applications, the amount of money involved in smart contracts is growing exponentially. However, smart contract faces many security threats due to its program characteristics and special execution environment. This paper proposes a formal verification method for smart contracts based on CPN. Firstly, the concept of data flow and control flow is proposed to better reflect the change of data state in the process of transaction execution. The simplified DAO contract is modeled hierarchically and the malicious behavior of attackers is reproduced by the simulation tools CPN Tools. Finally, the potential transaction vulnerabilities in the contract are successfully verified according to the analysis methods such as state space.

As a class of digital contracts, smart contracts are driven by data participation and have certain legal effects. A well-constructed smart contract behavior model must be able to meet the different needs of participants in terms of operational functions and data status. The data behavior that violates the data state requirements can reflect the defects of the smart contract. The more accurate the data attributes contained in the contract are, the more accurate the contract reliability can be judged from the data state. In combination with our current work, we intend to improve previously proposed WFDC-nets [Y, 2018] and define a novel Colored Petri net with Data Constraints(CFDC-net), among which the WFDC-net model for workflow analysis is extended to a general model that can be applied to a wide range of business processes and the different data attributes contained in the smart contract are formally defined. Then, the refinement model of multi-party and multiple transaction behaviors is explored to provide a model basis for behavior analysis, so as to ensure that the actual execution behavior of smart contracts is consistent with its data specification. In summary, formal verification of smart contract based on petri nets is of great significance. In the future, we will continue to carry out research on high petri nets aiming at security and optimization of smart contracts.

Funding The work is supported by Major Public Welfare Projects Foundation of Henan Province under Grant No.201300210200 and Open Foundation of Henna Key Laboratory Cryptography under Grant No. LNCT2020-A08.

Conflict of interest The authors declare no competing interests.

Author Contributions Yaqiong He and Hanjie Dong wrote the main manuscript text, and completed the experiment together, they are major contributor. Huaiguang Wu proposed constructive ideas and suggestions about this manuscript. Qianheng Duan prepared the introduction and background part and adjusted the grammar and sentence structure of the manuscript. All authors reviewed and approved the final manuscript.

Amani S, Bégel M, Bortin M, et al. (2018) Towards verifying ethereum smart contract bytecode in Isabelle/HOL[C]//Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs. pp: 66-77.
Blass E O, Kerschbaum F. Strain (2018) A secure auction for blockchains[C]//European Symposium on Research in Computer Security. Springer, Cham, pp: 87-110.
Bai X, Cheng Z, Duan Z, et al. (2018) Formal modeling and verification of smart contracts[C]//Proceedings of the 2018 7th international conference on software and computer applications. pp: 322-326.
Buterin V. (2014) A next-generation smart contract and decentralized application platform[J]. white paper,
Chinen Y, Yanai N, Cruz J P, et al. (2020) RA: Hunting for re-entrancy attacks in ethereum smart contracts via static analysis[C]//2020 IEEE International Conference on Blockchain (Blockchain). IEEE, pp: 327-336.
Dharanikota S, Mukherjee S, Bhardwaj C, et al. (2021) Celestial: A smart contracts verification framework[C]//2021 Formal Methods in Computer Aided Design (FMCAD). IEEE, pp: 133-142.
Duo W, Xin H, Xiaofeng M. (2020) Formal analysis of smart contract based on colored petri nets[J]. IEEE Intelligent Systems, pp: 19-30.
Ferreira Torres C, Iannillo A K, Gervais A. (2021) The eye of horus: Spotting and analyzing attacks on ethereum smart contracts[C]//International Conference on Financial Cryptography and Data Security. Springer, Berlin, Heidelberg, pp: 33-52.
Feng X, Wang Q, Zhu X, et al. (2019) Bug searching in smart contract[J]. arXiv preprint arXiv:1905.00799, 2019.
Garfatta I, Klai K, Graïet M, et al. (2021) A Solidity-to-CPN Approach Towards Formal Verification of Smart Contracts[C]//2021 IEEE 30th International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE). IEEE, pp: 69-74.
Garfatta I, Klai K, Graïet M, et al. (2022) Model checking of vulnerabilities in smart contracts: a solidity-to-CPN approach[C]//Proceedings of the 37th ACM/SIGAPP Symposium on Applied Computing. pp: 316-325.
Gehlot V, Nigro C. (2010) An introduction to systems modeling and simulation with colored petri nets[C]//Proceedings of the 2010 winter simulation conference. IEEE, pp: 104-118.
Kalra S, Goel S, Dhawan M, et al. (2018) Zeus: Analyzing safety of smart contracts[C]//Ndss. pp: 1-12.
Liu C, Liu H, Cao Z, et al. (2018) Reguard: finding reentrancy bugs in smart contracts[C]//2018 IEEE/ACM 40th International Conference on Software Engineering: Companion (ICSE-Companion). IEEE, pp: 65-68.
Liu Z, Qian P, Wang X, et al. (2021) Smart contract vulnerability detection: from pure neural network to interpretable graph feature and expert pattern fusion[J]. arXiv preprint arXiv:2106.09282, 2021.
Liu Z, Qian P, Wang X, et al. (2021) Combining graph neural networks with expert knowledge for smart contract vulnerability detection[J]. IEEE Transactions on Knowledge and Data Engineering.
Liu Z, Liu J. (2019) Formal verification of blockchain smart contract based on colored petri net models[C]//2019 IEEE 43rd Annual Computer Software and Applications Conference (COMPSAC). IEEE, pp: 555-560.
Ma RJ. (2018) On the Formal Description and Analysis of Security Protocols Using Colored Petri Nets[D]. Xidian University.
Mehar M I, Shier C L, Giambattista A, et al. (2019) Understanding a revolutionary and flawed grand experiment in blockchain: the DAO attack[J]. Journal of Cases on Information Technology (JCIT), pp: 19-32.
Nakamoto S. (2018) Bitcoin: A peer-to-peer electronic cash system[J]. Decentralized Business Review.
Park W S, Lee H, Choi J Y. (2021) Formal Modeling of Smart Contract-based Trading System[C]//2021 23rd International Conference on Advanced Communication Technology (ICACT). IEEE, pp: 48-52.
Pierro G A, Tonelli R. Paso (2020) A web-based parser for solidity language analysis[C]//2020 IEEE International Workshop on Blockchain Oriented Software Engineering (IWBOSE). IEEE, pp: 16-21.
Qian P, Liu Z, He Q, et al. (2020) Towards automated reentrancy detection for smart contracts based on sequential models[J]. IEEE Access, pp: 19685-19695.
Qu M, Huang X, Chen X, et al. (2018) Formal verification of smart contracts from the perspective of concurrency[C]//International Conference on Smart Blockchain. Springer, Cham, pp: 32-43.
Rodler M, Li W, Karame G O, et al. (2018) Sereum: Protecting existing smart contracts against re-entrancy attacks[J]. arXiv preprint arXiv:1812.05934, 2018.
Samreen N F, Alalfi M H. (2020) Reentrancy vulnerability identification in ethereum smart contracts[C]//2020 IEEE International Workshop on Blockchain Oriented Software Engineering (IWBOSE). IEEE, pp: 22-29.
Szabo N. (1997) Formalizing and securing relationships on public networks[J]. First monday, 1997.
Szabo N. (1996) Smart contracts: building blocks for digital markets[J]. EXTROPY: The Journal of Transhumanist Thought (16).
Sun T, Yu W. (2020) A formal verification framework for security issues of blockchain smart contracts[J]. Electronics.
Schneidewind C, Grishchenko I, Scherer M, et al. (2020) ethor: Practical and provably sound static analysis of ethereum smart contracts[C]//Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security. pp: 621-640.
T. A. Usman, A. A. Selçuk and S. Özarslan, et al. (2021) "An Analysis of Ethereum Smart Contract Vulnerabilities," 2021 International Conference on Information Security and Cryptology (ISCTURKEY), pp. 99-104, doi: 10.1109/ISCTURKEY53027.2021.9654305.
Tolmach P, Li Y, Lin S W, et al. (2021) A survey of smart contract formal specification and verification[J]. ACM Computing Surveys (CSUR), pp: 1-38.
Wang S, Ouyang L, Yuan Y, et al. (2019) Blockchain-enabled smart contracts: architecture, applications, and future trends[J]. IEEE Transactions on Systems, Man, and Cybernetics: Systems, pp: 2266-2277.
Wang Y, Gou G, Liu C, et al. (2021) Survey of security supervision on blockchain from the perspective of technology[J]. Journal of Information Security and Applications.
Y. He, G. Liu, D. Xiang, J. Sun, C. Yan and C. Jiang (2018) "Verifying the Correctness of Workflow Systems Based on Workflow Net With Data Constraints," in IEEE Access, pp. 11412-11423, 2018, doi: 10.1109/ACCESS.2018.2806884.
Ye J, Ma M, Lin Y, et al. (2020) Clairvoyance: cross-contract static analysis for detecting practical reentrancy vulnerabilities in smart contracts[C]//2020 IEEE/ACM 42nd International Conference on Software Engineering: Companion Proceedings (ICSE-Companion). IEEE, pp: 274-275.
Yu R, Shu J, Yan D, et al. (2021) ReDetect: Reentrancy Vulnerability Detection in Smart Contracts with High Accuracy[C]//2021 17th International Conference on Mobility, Sensing and Networking (MSN). IEEE, pp: 412-419.
Zou W, Lo D, Kochhar P S, et al. (2019) Smart contract development: Challenges and opportunities[J]. IEEE Transactions on Software Engineering, pp: 2084-2106.

No competing interests reported.

Download PDF

Version 1

posted

You are reading this latest preprint version

Formal verification of Reentrancy Vulnerability Based on CPN

Status:

Version 1

Abstract

Figures

1 Introduction

2 Background

2.1 Ethereum and smart contract

2.2 Features of Smart contracts

2.3 Colored Petri Net

2.4 The DAO Smart Contract

3 Property Specification And Model Building

3.1 Attribute specifications

3.2 Top-lever model

3.3 Attack-free Model

3.4 Attacker Model

4 Experimental Analysis Of The Dao Model

4.1 Non-secure state reachability analysis

4.2 CPN Tools State Space Analysis

4.3 CPN Tools status report analysis

4.4 CPN Tools State diagram analysis

4.5 Conclusion Verification Based on the Remix Platform

5 Related Work

5.1 Reentracy Vulnerability Detection

5.2 Formal verification of smart contract

6. Conclusion And Future Work

Declarations

References

Additional Declarations

Status:

Version 1