1 Introduction

Since Bitcoin was first introduced in 2009 [32], the blockchain has been regarded as a promising but yet challenging technology. According to a recent study by Garther [16], the market value for the blockchain-based technology can exceed $3.1 trillion by 2030. Many cloud platform giants such as Microsoft, IBM, Amazon, Oracle have proposed Blockchain-as-a-Service (BaaS) solutions to support various enterprise scenarios such as financial services and supply chains. These solutions are based on programs called smart contracts [40]. However, due to the openness of blockchain platforms, people have suffered some devastating consequence caused by the errors in smart contracts. For instance, the infamous The DAO exploit [4] resulted in the loss of almost $60 million worth of Ether, and the Parity Wallet error caused $169 million worth of Ether to be locked forever [41]. Obviously, unsafe smart contracts not only result in huge financial loss but also seriously undermine the confidence about the development of blockchain-based technologies.

Realizing the importance of safe and secure smart contracts, researchers have conducted various types of studies [25, 27, 44] to reveal the nature of unsafe smart contracts as well as to detect such problems. As reported, many common vulnerabilities in the blockchain domain are related to nondeterminism [46], which is actually caused by concurrent calls. Model checking [17] has been successfully applied in the verification for many modern software systems with the concurrency feature. Generally, model checking techniques can be used to check various properties expressed by temporal logics [28], including safety properties and liveness properties. A safety property specifies that something bad never happens, while a liveness property specifies that something good will eventually happen, playing an important role in the correctness of smart contracts. Security requirements are usually a kind of safety properties.

While model checking techniques are promising for reducing the potential threats and errors of smart contracts, they currently require the skill of writing formal models and logic formulas, which is challenging for engineers who do not have solid mathematical background. Learning how to write formal models and specifications increases the learning curve and thus reduces the applicability of these techniques. We propose in this paper a novel framework mcVer to ease the difficulty of using model checking techniques and deal with the diversity of smart contract properties.

Our framework mcVer uses model checking tool VERDS  [50] as the foundation to support the verification of smart contracts written in Solidity, which is a smart contract language of Ethereum [47]. The contributions of this paper are summarized as follows.

  1. 1.

    The mcVer framework is able to verify not only safety properties but also liveness properties of smart contracts. For the properties that are not satisfied, mcVer produces a counter example by showing a sequence of statements in the original Solidity program as a hint for fault localization.

  2. 2.

    We provide automatic verification for smart contracts by means of the automatic transformation from a subset of the Solidity language to the modeling language of VERDS.

  3. 3.

    We implement the framework and apply it to several case studies, including checking some typical security vulnerabilities and verifying properties, including liveness properties, of an access control smart contract [51].

The remainder of this paper is organized as follows. Related work is reviewed in Sect. 2. Solidity and VERDS are introduced in Sect. 3. We present the general idea of mcVer framework in Sect. 4 and illustrate the technical details in Sects. 5, 6 and 7. Case studies and experiments are shown in Sect. 8. Section 9 concludes and discusses limitations of mcVer  and the future work.

2 Related Work

Luu Loi [27] and Atzei [9] summarized several types of common security vulnerabilities, such as Transaction-Ordering Dependency (TOD) and Reentrancy Vulnerability. Based on these types of common security vulnerabilities, a number of research efforts have been made to ensure the safety and security for smart contracts. The most explored are testing based techniques [21, 48] and static analysis-based techniques, usually based on the symbolic execution, including Oyente [27], Securify [45], Slither [18], ETHBMC [20], Mythril [42], SolMet [22], SmartCheck [43], Ethainter [12], Manticore [30], VeriSmart [38] and FAIRCON [26]. However, these approaches heavily depend on known security patterns to detect errors and cannot guarantee the functional correctness in blockchain-based applications.

To overcome the limitation of above-mentioned approaches, formal verification techniques [15] have been proposed to verify the correctness of smart contracts. Research on formal verification of smart contracts starts with theorem proving based approaches. Hirai [24] uses theorem prover Isabelle [35] to verify smart contracts [23] and uses the Lem [31] to define a formal model for the Ethereum virtual machine (EVM). Bhargavan et al. [11] convert Solidity and EVM bytecode contracts into functional programming language F* [39]. Nehai et al. [34] translate smart contracts into models of Why3 [19]. The verification procedures in this kind of approaches generally require user’s interaction and are difficult to deal with liveness properties. The verification procedure of mcVer  is automatic and not only safety properties but also liveness properties can be verified in mcVer.

Model checking based techniques are also studied by many researchers. Albert et al. [7] use existing verification engines developed for C programs [10] to verify safety properties of low-level EVM code. Sukrit Kalra et al. [25] present ZEUS, which uses bounded model checking techniques to verify safety properties of smart contracts. Anton Permenev et al. [36] present VerX, which combines reduction of temporal safety verification to reachability checking, with symbolic execution and delayed abstraction. Mavridou [29], Nehai [33] and Abdellatif [8] present their work based on the model checking tool NuSMV [14]. A model-based framework VeriSolid is proposed in [29], which focuses more on the code generation procedure rather than verifying Solidity source code. Authors of [33] and [8] present work that verifies particular smart contracts. The former focuses on the contracts in the energy market field and the latter tries to verify a supply chain management smart contract. The NuSMV based methods are possible to deal with more properties, but existing work does not provide methodological techniques to support the verification of commonly developed contracts. Our framework mcVer  is able not only to verify various properties but also implements the related tool to smooth the verification procedure that starts directly from the Solidity source code. The tool may return a counter example when a property is not satisfied, providing a further help for debugging. To the best of our knowledge, none of the formal method based work for the verification of smart contracts is able to provide such a functionality.

3 Solidity and VERDS 

3.1 Solidity

Fig. 1.
figure 1

aucSC, a smart contract for auction.

Full size image

Solidity is a programming language developed to write smart contracts that run on the EVM. A Solidity smart contract mainly consists of two parts, the variable declaration and the function definition. The former defines state variables used by the contract and the latter specifies the potential behavior of the contract. Figure 1, for example, shows partial code of our running example, aucSC, a simple auction contract modified from [1].

State variables of a smart contract are variables whose values are permanently stored in the blockchain and each has a type. For example, variables bene and hBidder, indicate addresses of the beneficiary and the current highest bidder of the auction, respectively. Variable hBid denotes the current highest bid and variable ended indicates whether an auction is ended or not.

Besides global state variables, there are implicit global variables that are defined by the EVM, including related accounts and balances. Once an account is created on the blockchain, it has an address as its identification and a variable to record the changes of its balance. When an account uses a smart contract, its address is the value of msg.sender, which is used but not defined in the contract. See aucSC for example. Accounts related to a smart contract include the account that deploys it (its owner), the accounts that use it (its users), and some accounts specified by the contract, e.g. the address of the beneficiary in sucSC. The balances related include its own balance and balances of the related accounts.

A function consists local variable declaration and statements. Functions can receive data via parameters, perform computation, manipulate state variables, and interact with other accounts. Functions are defined to operate on the states of the contract. The constructor() is a special function that is executed only once when the contract is deployed on the blockchain. The account who calls constructor() is the owner of the contract. Other functions can be called and executed many times during the lifecycle of the contract. For example, function bid(), which defines the bidding behavior, can be executed by arbitrary number of users before aucEnd(), which sets variable ended to be true. A function may also operate on the implicit global variables. An execution of a function may receive msg.value amount of money from its trigger msg.sender, and change the balances of related accounts.

We consider a subset of Solidity language that are sufficient to express most contracts. The supported subset is summarized in Fig. 2.

Fig. 2.
figure 2

Subset of Solidity language mcVer supports

Full size image

A call to a function of a contract activates an execution. The execution terminates after successfully updating the state of blockchain, or aborting and rolling back to the state before the call. While smart contracts allow the concurrent calls, the executions of concurrent calls are sequential due to the execution model of EVM [37]. We take this into account when formalize smart contracts.

3.2 Model Checking Tool VERDS 

Model checking is considered one of the most practical applications of theoretical computer science in the verification of concurrent systems. The basic idea of model checking is to use the state transition system (S) to represent the behavior of the system, and the modal formula (F) to describe the properties of the system. In this way, the question of whether the system has the desired properties can be transformed into a question of whether S satisfies F. For finite state systems, this problem is algorithmically decidable. We use VERDS as the verification engine. VERDS is a model checking tool that has been applied in many aspects, such as the verification of SystemC design [49] and the verification of multi-agent systems [13]. The input to a model checking tool usually includes a system model and a specification. The modeling language of VERDS is called VERDS modeling language (VML). A verification model specified in VML is called a VERDS verification model (VVM), including a system model defined by the guarded command transition systems and specifications expressed by the computation tree logic (CTL).

Suppose p is any propositional atom, then CTL has the syntax given as follows.

$$\begin{aligned} \varPhi ::=&p|\lnot \varPhi |\varPhi \wedge \varPhi |\varPhi \vee \varPhi |A\varPsi |E\varPsi \\ \varPsi ::=&X\varPhi |F\varPhi |G\varPhi |(\varPhi U \varPhi ) \end{aligned}$$

Among them, \(\varPhi \) is the CTL formula and \(\varPsi \) is the auxiliary path formula. The set of operators of CTL formula is divided into path operators and temporal operators. There are two kinds of path operators: \(A\varPsi \) indicates that on all paths \(\varPsi \) should be true, and \(E\varPsi \) indicates that \(\varPsi \) should be true on at least one path. The temporal operators are X, F, G, U. Two kinds of temporal operators are used in this paper: \(F\varPhi \) indicates that \(\varPhi \) will eventually be true on a certain state on a path; \(G\varPhi \) indicates that \(\varPhi \) should be satisfied for all the states on a path. Properties to be checked on guarded transition system can be of various kinds:

  • safety: ‘something bad never happens’ is usually expressed in CTL as \( AG (\lnot p)\);

  • liveness: ‘something good will eventually happen’ is usually expressed in CTL as \( AF ( p)\).

Each VVM consists of six parts: global alias definition, global variable declaration, initialization, module definition, process instantiation, and property specification. These six parts are distinguished by keywords DEFINE, VAR, INIT, MODULE, PROC and SPEC, respectively. Variables should be bounded.

A module in VVM is a template of a transition system, defined under keyword MODULE. Each module consists of four parts: module identifier and list of parameters, local variables declaration (VAR), local variables initialization (INIT), and collection of transitions (TRANS). A transition consists of two parts: logical expressions (guard) and assignments (command). When the logical expression is true, the assignment statement will be executed atomically. When logical expressions in different transitions are true at the same time, a random one of them will be executed. A process in PROC part is an instance of a module; a local variable x in a process p0 can be accessed using the form p0.x. Properties under verification are specified in SPEC part. If a property does not hold, a counterexample can be found in the CEX file returned by VERDS.

4 Overview of mcVer  Framework

Fig. 3.
figure 3

Overall framework of mcVer.

Full size image

The framework of mcVer is shown in Fig. 3, in which our main contributions are in boxes with purple border. The smart contract under verification are either entirely or partly translated into the VAR, INIT, and MODULE parts of a VVM; the scenario corresponds to the PROC part, and the specification is formulated as CTL formulas in the SPEC part. The model checker VERDS is then used to verify whether the smart contract satisfies required properties. If a property is not satisfied, VERDS returns the trace indicating the problematic behavior in a CEX file. A counter example on the Solidity level is then extracted from it.

We present Smart contract modeling in the next section, Scenario Configuration and Specification Formulation in Sect. 6, and Counter Example Extraction in Sect. 7. Smart contract aucSC (Fig. 1) will be used as running example to help illustrating our ideas. Part of its corresponding VVM, aucVVM, is shown in Fig. 4. Details will be explained in the later sections.

Fig. 4.
figure 4

aucVVM, the corresponding VVM of aucSC.

Full size image

5 Smart Contract Modeling

The behavior of smart contracts is defined by the guarded command transition system. To be intuitive, we describe the semantics of smart contracts directly with the VML. We discuss key points of mapping behavior of the EVM, variables, functions and function call in smart contracts to VVMs in this section.

Behavior of EVM. Due to the execution model of EVM, transactions are executed in a single-threaded manner. A boolean variable \( pCtrl \) is declared to control the execution of processes and is false by default. Only when \( pCtrl \) is true, a process except for that of constructor can move to the next step. When a process ends its execution, it releases the control by setting \( pCtrl \) to be true. Function constructor executes only once before all other functions. It needs not to check \( pCtrl \) to go. For example, a process instantiated from module bid in Fig. 4 is waiting until the control variable \( pCtrl \) becoming true (Line 38) to start its execution and change \( pCtrl \) to be false to block other process. It sets \( pCtrl \) to be true at the end of its execution (Line 51).

Related balances are explicitly defined as a global array balance in VVM. They are defined at Line 5 and initialized at Line 13 in Fig. 4, for example. The trigger address msg.sender and the amount of money msg.value are modeled as two parameters of each module in the VVM. See Line 34 in Fig. 4 for example. Changes of balances of related accounts are coded in the last transition of the module of each function.

State Variables. State variables of smart contracts are accordingly defined as bounded integer (in the VAR part) and initialized (in the INIT part) in the VVM. For readability, we use characters to represent the values of variables with address type. The address of contract under verification is set to be ‘Z’ by default. For example, Lines 3–4 and 11–12 in Fig. 4 are definition and initialization of state variables of aucSC in aucVVM. Constants is defined in the DEFINE part.

Table 1. Statements mapping
Full size table

Functions. A function in a contract is modeled by a module in VVM, which is a guarded command transition system. By this we in fact define a transition system semantics for the behavior of contracts. Let S be the set of statements in a function and \(P_s\) be the label of statement s. Each statement in \(S\) is modeled as one or multiple transitions in VVM. Each module in VVM has an extra local variable pc to model the change of \(P_s\). The mapping of statements in the subset of Solidity (Fig. 2) to VML is shown in Table. 1. The module in VVM of bid() in aucSC (Fig. 1) is shown in Fig. 4 (Lines 34–51). Line 34 declares the module identifier.

Fig. 5.
figure 5

Illustration of function call.

Full size image

Function Call. We use shared variables to handle calls between functions, which may be in the same contract or not. The caller and callee can execute in parallel, with the blocking feature. Once one function is active, the other one is blocked. Some callees may return uncertain values because they are defined outside and controlled by the environment, such as functions transfer() and send(). We model this uncertainty by using non-deterministic choice of transitions in a module.

A module to model function send() called in bid() in aucSC is shown in Lines 52–60 in Fig. 4, for example. Auxiliary variables sta, rtv, rcv and amount are defined as global variables (Lines 8–9) to model starting or ending the process, returned value, the address of the sender and the amount of money sent, respectively. A process of module send() starts when \(sta=1\) and sets sta to 0 and returns rtv when it finishes. At Lines 57 and 58, VERDS randomly chooses one transition to execute and so is the value of rtv. This makes the returned value non-deterministic. When bid() is trying to call send() (Line 42), it sets sta to 1 and then the execution does not resume until sta becomes 0. The interaction between the caller and the callee in a function call is depicted in Fig. 5.

6 Scenario Configuration and Specification Formulation

6.1 Scenario Configuration

A scenario defines how a contract is used. Since smart contracts are deployed on the blockchain, which is an open environment, the order of calls to its functions are not deterministic. This uncertainty is modeled as concurrency in mcVer. In some cases, e.g. sequential transactions submitted by the same account, the corresponding functions, i.e. callees, should be scheduled to execute sequentially.

We propose a scenario definition language (SDL), which is simple but capable of expressing both sequential and concurrent executions of function. Sequential execution of functions is separated by line shift and concurrent execution of functions is separated by symbol ‘|’. For example, in contract aucSC shown in Fig. 1, users can only call function bid() after the contract has been deployed. After its deployment (constructor()); there may be multiple users bidding at the same time; the owner may call function aucEnd() to end it. Suppose the owner is A and there are three bidders B, C and D bidding with amount 2, 3, 4, respectively. After the owner has deployed the contract on the blockchain, the three bidders can bid in any order. Then the owner ends the auction. The scenario, named aucSNR, is formulated in SDL as:

$$\begin{aligned}&p0: constructor(A,0,A)\\&p1: bid(B,2)\;|\;p2:bid(C,3)\;|\;p3:bid(D,4)\\&p4: aucEnd(A,0) \end{aligned}$$

This scenario is then translated into the PROC part of the VVM (Lines 18–23 in Fig. 4). The three biddings can be executed in any order, but can only be executed sequentially due to the execution model of the EVM. The execution order is controlled by variable order. The variable level i indicates how many processes have been executed so far under order = i. Intuitively, variable order controls line execution, while level i controls the execution of processes in the same line. For scenario aucSNR, for example, we have \(level{\textbf {0}}\in [0,1]\) and \(level{\textbf {1}}\in [1,3]\) because only one process p0 is executed under \(order=0\) but three concurrent processes p1, p2, p3 are executed under \(order=1\). A process control module porderctrl() is used to help execution order (Lines 27–33 in Fig. 4).

6.2 Specification

Specifications of smart contracts are defined under scenarios. For example there are some basic requirements for the aucSC contract:

  1. 1.

    Eventually there is a bidder win (liveness property);

  2. 2.

    The winner is always the bidder with the highest bid (safety property).

The requirements demand that after the auction is ended, 1) there is a winner and the winner must be one of the bidders, and 2) the winner must be the bidder with highest bid. Consider above mentioned scenario. There are three bidders. One of them will win. That is, \( hBidder =B\), C or D. The bidder D pays the highest bid. When the value of the order reaches the maximum, 3 in this scenario, all processes are executed and the scenario finishes. We use a keyword \( End \) to indicate that the involved scenario is ended. Therefore, the requirements formulated under aucSNR are expressed by the following CTL formulas:

  1. 1.

    aucPr1: \( AF (( End ) \& (( hBidder =B)|( hBidder =C)|( hBidder =D)))\);

  2. 2.

    aucPr2: \( AG (!( End )|( hBidder =D))\).

Where !p|q is equivalent to \(p\;implies\;q\). The specifications written in CTL formulas are used in the SPEC part of the VVM, shown in Fig. 4 (Lines 25–26).

7 Verification and Counter Example Extraction

The generated VVM is then verified by VERDS. If a property is satisfied, we can guarantee that the contract meets the corresponding requirement under the given scenario. Otherwise, VERDS may return a CEX file that records the trace of a counter example. A trace is a sequence of states generated by an execution of the contract. The procedure of counter example extraction starts from the trace. By the values of variables in states, we find the corresponding transitions in the VVM. Then according to Table 1, a reverted procedure of contract modeling is used to map the transitions to the Solidity contract. As such we have a counter example on the Solidity level. Below we illustrate the procedure by an example.

Fig. 6.
figure 6

A trace returned by VERDS.

Full size image

By manually checking the aucSC contract (Fig. 1), it seems that it meets the second requirement (aucPr2). The result of the verification under scenario aucSNR, however, shows otherwise. That is, aucSC does not always choose the bidder with the highest bid as a winner. The trace returned by VERDS is shown in Fig. 6. The trace shows that when the three bidders bid sequentially in the order of bidder B, bidder C and then bidder D, the winner is bidder B. The corresponding order of calls on aucSC is shown in Fig. 7. Statements with process identifiers, i.e., p0, ..., p3 and p4, on the left are executed but the gray statements are not in a trace for a counter example.

Fig. 7.
figure 7

A counter example of aucSC.

Full size image

When bidder B bids, p1 : bid(B, 2) is called. At state S7, where \(p1.pc=3\) and \(hBid=0\), the condition of transition at Line 45 of aucVVM (Fig. 4) is satisfied, then p1.pc is changed to 7, corresponding to the transition of Line 46 of aucVVM. By the information of the transitions in aucVVM, we then can find that after Line 13 of aucSC (Fig. 1), the execution go to Line 16, skipping Line 14, where is the gray line in Fig. 7.

The execution trace of bid(C, 3) and bid(D, 4) from the states shown in Fig. 6 to the execution path shown in Fig. 7 can be similarly explained.

In the counter example, after the first bidder, say, with bid 2, other higher biddings 3 and 4 may be aborted because the send operation fails. Recall that the return value of send() depends on what happens outside the contract and may return true or false nondeterministically. The subtle potential error is revealed by the counter example.

8 Case Studies and Experiments

We implemented mcVer and applied it to several case studies, including some reported contracts with typical security vulnerabilities [2, 3, 6] and an access control smart contract [51]. Our experiments are carried out on a machine with 3.10 GHz CPU, 512 GB RAM. The dataset is available on [5].

8.1 Security Vulnerabilities Checking

We show in this section some examples to illustrate how vulnerabilities such as Transaction-Ordering Dependency (TOD) and Reentrancy Vulnerability are revealed in mcVer.

Transaction-Ordering Dependency. Assume two transactions invoke a contract at the same time. If a final state depends on the order of these transactions, then a TOD vulnerability may exist. An attacker can enforce a specific execution order to make profit [27].

Fig. 8.
figure 8

A contract with TOD [6], todSC

Full size image

An example of a contract with TOD vulnerability [6] is shown in Fig. 8. Suppose the reward is first set to 3 by the owner A after the contract is deployed. Then user B sees the reward and tries to claim, and at the same time the owner resets the reward to 1. These two transactions may be executed in any order. The contract is first translated into a VVM with a module setReward(msg_sender, msg_value) to model function setReward(), a module claimReward(msg_sender, msg_value, submission) to model function claimReward(uint submission) and a module to model the constructor. The aforementioned scenario is configured as:

$$\begin{aligned}&p0:EthTxOrderDependenceMinimal(A,0)\\&p1:setReward(A,3)\\&p2:setReward(A,1)|p3:claimReward(B,0,3) \end{aligned}$$

Suppose user B has a balance 5 before a transaction. After that, he should expect a balance to be 8, since the reward is 3 when he submits the transaction. Therefore, the property is denoted as follows.

$$AG(!( End )|(balance[B]=8))$$

VERDS exhaustively explores the state space of the model and finds violation of the property. Therefore, a trace where the user’s balance is only 6 at the end of the scenario is returned by VERDS as a counter-example. The trace shows that setReward() is executed before claimReward() and the reward is set to 1. Then, should B always have balance of 6 after the scenario? Verification of the following property shows otherwise, because claimReward() may also be executed first.

$$AG(!( End )|(balance[B]=6))$$

The results show that a different execution order may lead to different balance of B. The TOD vulnerability is detected.

Reentrancy Vulnerability. If a function of a contract is called again before its previous invocations complete execution and the next call leads to inconsistency of balances of related accounts, a Reentrancy Vulnerability exists in the contract. The reason of TheDAO event is exactly that the Reentrancy Vulnerability in the DAO was exploited by attackers. A contract with Reentrancy Vulnerability is shown in Fig. 9. When function withDraw() is called, the statement msg.sender.call.value(amount)() in Line 8 will transfer some money to another contract and trigger its fallback function. When there is a callback to withDraw() in the fallback function, a reentrancy is formed and an attacker may withdraw more amount of money than his balance in the contract.

Fig. 9.
figure 9

Contract with reentrancy [3], reSC

Full size image

The contract is translated into a VVM with a set of modules. We set the number of callbacks to 1, because if there is a re-entry it will be found in one callback. An extra module fallback() is used to model fallback function in the external contract which is triggered automatically by withDraw(), and a module \(withDraw\_back()\) is used to model the re-invoked withDraw() in fallback function. Suppose a user B first deposits 2 wei (a unit of Ether) into the contract by invoking receiveEther() and then withdraws his money. The scenario is configured as follows.

$$\begin{aligned}&p0:receiveEther(B,2)\\&p1:withDraw(B,0) \end{aligned}$$

Suppose the initial balance of the user is 5, the required property is that his balance after the execution of the scenario is still 5. This property is formulated as follows.

$$\begin{aligned} AG(!( End )|(balance[B]=5)) \end{aligned}$$

Checking this property with the above scenario, mcVer  returns with false, meaning that the balance of the user is inconsistent before and after the scenario. The Re-entrancy Vulnerability is then detected.

Table 2. Checking time for security vulnerabilities.
Full size table

Experimental Results. Table 2 shows the time required for mcVer to detect the vulnerabilities contained in the above four cases. The bound of number of addresses, MaxD, and the bound of integer, MaxI, are shown in the third colomn. The procedures of model extraction and counter example generation are very fast, and the times required for verification of them are within several seconds.

8.2 Access Control Contract

The previously discussed properties related to security are all safety properties. In this section we study an access control contract [51] to show that mcVer  can also deal with liveness properties.

Problem Description. The ubiquitous interconnection of physical objects has significantly accelerated data collection, aggregation, and sharing, making Internet of Things (IoT) one of the most basic architectures for applications in the smart health-care, smart transportation, and home automation domains. However, such interconnection may also bring serious security problems to IoT systems. If a system does not have secure access control, through intrusion into the system, unauthorized entities (attackers) can illegally access existing IoT devices by simply deploying their own resources. Therefore, the access control issue of the IoT has received extensive attention from academia and industry. The access control system should satisfy the following four requirements:

PR1.:

Regardless of whether a user has rights or not, the system should return a result;

PR2.:

Users who have no right to access can’t get access rights;

PR3.:

Users with access rights can always obtain access rights;

PR4.:

Only specific users (such as administrators) can modify users’ access rights.

Fig. 10.
figure 10

Access control contract [51].

Full size image

We outline the contract and show it in Fig. 10. There are five global variables, among which owner, subject and object indicate the address who deployed the contract, the address of the accessing user and IoT device bound to the contract, respectively; the variables policies with mapping type are used to record the access policies. There are also three main functions in this contract. Function AcessControlMethod() is the constructor, initializing owner, subject and object. Function policyAdd() is used to add new access policy. Function policyUpdate() is used to update the access permissions in an access policy. Function accessControl() is used to get access rights. There is a local variable err in accessControl() representing whether a user can get access right. Different values of err represent different return results as shown in the following list.

  1. 1.

    \(err=0\) means right is granted;

  2. 2.

    \(err=1\) means punishment isn’t ended and right is not granted;

  3. 3.

    \(err=2\) means user has no permission and right is not granted;

  4. 4.

    \(err=3\) means that although the user has the permission but he will be punished and right isn’t granted, because he visits too frequently;

  5. 5.

    \(err=4\) means user has no permission and visit too frequently in the minimal interval, will be punished, right isn’t granted;

  6. 6.

    \(err=5\) means the device that the user wants to visit is not current device and right isn’t granted.

Modeling. For the verification of aforementioned four basic properties, we design three different scenarios. The first scenario, denoted by SNR1, is defined as:

$$\begin{aligned}&p0:constructor(A,0,B)\\&p1:policyAdd(A,0,R,Y,2,2)\\&p2:policyUpdate(A,0,R,N)| p3:accessControl(B,0,R,2) \end{aligned}$$

In this scenario, administrator A deploys a contract for user B. He then sends a transaction calling policyAdd to add a new policy which allows B to read (R) the data on resource with identifier 3. This policy allows the user to visit the resource twice in interval 2 units of time. Then B tries to get access right and A tries to withdraw the permission for user B at the same time. Scenario SNR1 can be used to check properties PR1 and PR3, which are concretized and specified respectively by SNR1.pr1 and SNR1.pr2, shown as follows.

$$ \begin{aligned} \text {SNR1.pr1: }&AF (( End ) \& (p3.err=0 | p3.err=1 | p3.err=2 | p3.err=3 | p3.err=4 | p3.err=5))\\ \text {SNR1.pr2: }&AG (!( End )|(p3.err=0)) \end{aligned}$$

The second scenario, SNR2, is defined as:

$$\begin{aligned}&p0:constructor(A,0,B)\\&p1:policyAdd(A,0,R,Y,2,2)\\&p2:policyUpdate(A,0,R,N)\\&p3:accessControl(B,0,R,2) \end{aligned}$$

After policyAdd finishes, policyUpdate withdraws the permission of user B. The B tries to access the resource. Scenario SNR2 can be used to check properties PR1 and PR2, which are concretized and specified respectively by SNR2.pr1 and SNR2.pr2, shown as follows.

$$ \begin{aligned} \text {SNR2.pr1: }&AF (( End ) \& (p3.err=0 | p3.err=1 | p3.err=2 | p3.err=3 | p3.err=4 | p3.err=5))\\ \text {SNR2.pr2: }&AG (!( End )|(p3.err=2)) \end{aligned}$$

The last scenario, SNR3, describes the situation that a user B with no permission tries to update his own permission and then tries to get access right:

$$\begin{aligned}&p0:constructor(A,0,B)\\&p1:policyAdd(A,0,R,N,2,2)\\&p2:policyUpdate(B,0,R,Y)\\&p3:accessControl(B,0,R,2) \end{aligned}$$

Scenario SNR3 can be used to check properties PR1 and PR4, which are concretized and specified respectively by SNR3.pr1 and SNR3.pr2, shown as follows.

$$ \begin{aligned} \text {SNR3.pr1: }&AF (( End ) \& (p3.err=0 | p3.err=1 | p3.err=2 | p3.err=3 | p3.err=4 | p3.err=5))\\ \text {SNR3.pr2: }&AG (!( End )|(p3.err=2)) \end{aligned}$$

The changes of permission can only be checked by the returned error code of accessControl(), so in this scenarios p3 is added and the formula SNR3.pr2 is the same as SNR2.pr2.

Table 3. Verification results for access control contract.
Full size table

Verification. After the contract, the scenarios and the property specification are translated into VVM, we verified the VVM using VERDS. The results are shown in Table 3. The first column list the names of requirements, the second column lists the related CTL formula, the third and forth columns are verification results, and the last column shows verification time for each property. The result for PR1 is true only when the verification results of SNR1.pr1, SNR2.pr1 and SNR3.pr1 are all true. From the results, we know that the contract doesn’t meet PR3 and PR4. And the counter-example returned when verifying SNR3.pr2 shows that user B, who is not an administrator, successfully changes his own permission by calling function policyUpdate(), and gets the access right which violates PR4. All six properties are verified in about two minutes.

9 Conclusion and Future Work

In this paper, the model checking based framework, mcVer, has been proposed to support the verification of smart contracts written in Solidity. mcVer is able to verify a variety of properties of smart contracts. For the properties that are not satisfied, mcVer produces a counter example by showing a sequence of statements in the original Solidity program as a hint of where a faulty statement may be located. We have implemented mcVer and applied it to automatically checking various types of security vulnerabilities and properties of an access control smart contract. The results show that the proposed framework is flexible and efficient and can facilitate software development in the blockchain domain in terms of the diversity of detecting software breaches.

The limitations of mcVer  framework come from two folds. The first is from the model checking technique itself, which can only deal with bounded systems and may suffer from state explosion issue when the model scales up. The second is that we have to configure the scenarios with particular values of parameters, which confines the space to be explored and limits the ability of mcVer. In the future, we will study the property-based contract modeling technique to reduce the size of the model to be verified and consider a better way to model the environment and user behaviors to broaden the scope of verification. Also, we will consider the impact of gas limitation to the behavior of contracts.