Debugging Smart Contract's Business Logic Using Symbolic Model-Checking

TL;DR

This paper introduces a symbolic model-checking approach for verifying the correctness of smart contract business logic, addressing a critical gap left by existing tools that focus only on implementation bugs.

Contribution

It presents a novel formal verification method for Solidity smart contracts that can verify both state and trace properties, including business logic correctness.

Findings

Detected a non-trivial business logic error in MiniDAO smart contract within seconds

Demonstrated effectiveness of the approach on real-world smart contract example

Addresses a significant gap in existing smart contract verification tools

Abstract

Smart contracts are a special type of programs running inside a blockchain. Immutable and transparent, they provide means to implement fault-tolerant and censorship-resistant services. Unfortunately, its immutability causes a serious challenge of ensuring that a business logic and implementation is correct upfront, before publishing in a blockchain. Several big accidents have indeed shown that users of this technology need special tools to verify smart contract correctness. Existing automated checkers are able to detect only well known implementation bugs, leaving the question of business logic correctness far aside. In this work, we present a symbolic model-checking technique along with a formal specification method for a subset of Solidity programming language that is able to express both state properties and trace properties; the latter constitutes a weak analogy of temporal properties. We evaluate the proposed technique on the MiniDAO smart contract, a young brother of notorious TheDAO. Our Proof-of-Concept was able to detect a non-trivial error in the business logic of this smart contract in a few seconds.

Equations

$$function{f}_i(ar{g}_0,ar{g}_1,...,ar{g}_n)public[payable][return(T)]$$

$$trace(\sigma )=\forall i\in \mathbb{N},0\le i<len(\sigma ).\delta ({\sigma }_i,{\sigma }_{i+1})$$

$$\Delta =\{({\sigma }_i,{\sigma }_j):\exists (f^{\prime },f_{pre})\in {\Phi }_{pre},v,s,t,p.{\sigma }_j=f^{\prime }({\sigma }_i,v,s,t,p)\wedge f_{pre}({\sigma }_i,v,s,t,p)\}$$

$$\forall {\sigma }_0\in I.P({\sigma }_0)\wedge \forall {\sigma }_i,{\sigma }_j\in \Sigma .(\delta ({\sigma }_i,{\sigma }_j)\wedge P({\sigma }_i))\to P({\sigma }_j)$$

$$\forall {\sigma }^{\ast }\in {\Sigma }_k^{\ast },i\in \mathbb{N}.i\le len({\sigma }^{\ast })\to P({\sigma }_i^{\ast })$$

$$P({\sigma }^{\ast })=\exists i,j\in \mathbb{N}.{\sigma }_i^{\ast }[eventlog]=E_1\wedge {\sigma }_j^{\ast }[eventlog]=E_2\wedge i<j\le len({\sigma }^{\ast })\to$$

$$\forall k\in \mathbb{N}.i<k<j.{\sigma }_k^{\ast }[eventlog]\ne E_3$$

$$P({\sigma }^{\ast })=\exists i,j\in \mathbb{N}.{\sigma }_i^{\ast }[eventlog]=E_1\wedge {\sigma }_j^{\ast }[eventlog]=E_2\wedge i<j\le len({\sigma }^{\ast })\to$$

$$\forall k\in \mathbb{N},i<k<j.f_{pre}({\sigma }_k^{\ast },v,s,t,p)=True$$

$$trans$$

$$\underset{j=1}{\overset{|{\Phi }_{pre}|}{\bigvee }}(f_j^{pre}({\sigma }_i,v_i,s_i,t_i,p_i)=True\wedge {\sigma }_{i+1}=f_j^{\prime }({\sigma }_i,v_i,s_i,t_i,p_i))$$

$$path({\sigma }_{[\mathrm{0..}k]})=\underset{0\le i<k}{\bigwedge }transition({\sigma }_i,{\sigma }_{i+1})$$

$$NoSelfAddrCall=\underset{i=0}{\overset{k-1}{\bigwedge }}(s_i\ne contractAddr\wedge s_i\ne noAddr),$$

$$NotVotedRefund(\sigma )=\exists i,inv,s,1\le i<k.{\sigma }_{cs}^i[logs]=Deposited(inv,s)\wedge$$

$$\exists j,in{v}_1,s_1,id,1\le j<k.{\sigma }_{cs}^j[logs]=ProposalAdded(in{v}_1,s_1,id)\wedge$$

$$\forall n,i{d}_1,1\le n<k.{\sigma }_{cs}^n[logs]\ne Voted(inv,i{d}_1,True)\wedge$$

$${\sigma }_{cs}^n[logs]\ne Voted(inv,i{d}_1,False)\wedge$$

$${\sigma }_{cs}^n[logs]\ne Refund(inv)\wedge {\sigma }_{cs}^n[logs]\ne Transfer(inv)\to$$

$$\forall m,i\le m<k.refun{d}_{pre}({\sigma }_m,v,inv,t,p)$$

$$InvDaoBalance({\sigma }_k)=\sum _{i\in Addr}{\sigma }_{cs}^k[daoBalance[i]]=daoTokensEmitted$$

$$RejectedNotExecuted(\sigma )=\forall n.\exists i,j\in N.{\sigma }_{cs}^j[logs]=ProposalAdded(n,amount)\wedge$$

$${\sigma }_{cs}^j[logs]=ProposalRejected(n)\wedge i<j\to \forall k,i<k<j.$$

$${\sigma }_{cs}^k[logs]\ne ProposalExecuted(n)$$

Full text

1 Introduction

In 2008, Satoshi Nakamoto 111This is a pseudoname. Real name of this crypto enthusiast is still unknown. published a paper where he described an architecture of fully distributed decentralized paying system called Bitcoin [14].

Bitcoin is a distributed ledger of user balances in essence. What makes this system really unique is an inherited possession of several properties, namely massive fault-tolerance, censorship-resistance, authenticity of data and transparency of operations.

A family of systems that inherits main Bitcoin traits is now known under a term blockchain. Shortly after Bitcoin gained traction, it became clear that the blockchain can be used not only as a distributed ledger of user balances, but also as a distributed computation platform that is able to execute some business logic by reacting on user inputs and maybe exchange value between participants in a form of crytocurrency transfers.

The very first project that has implemented this idea was Ethereum [7]. A business logic in its context is called a smart-contract, where user inputs are called transactions.

Immutability and transparency of smart contracts provides never seen before level of trust for end users enabling an emergence of new kind of business models built on top of this technology. Unfortunately, its immutability turns out to be a threat in some cases: if an error sneaked in a smart contract, and developers failed to find it before publishing the contract in a blockchain then there will be no way to fix it afterwards, while an attacker is able to exploit the error in any suitable moment.

TheDAO attack [3] has demonstrated that this is indeed the case. The attack led to money loss as big as 60 million dollars in crytocurrency. There were yet more several big accidents since then [1] [2]

This issue presents a serious threat to a wide technology adoption and is currently well understood by the Ethereum community and other users. At this moment, if you are a smart contract developer and would like to ensure that your contract is reliable, you have two options: either apply for a manual human-driven audit in some blockchain security company or use any of available automatic checking tools that scan your source code for typical error patterns such as integer overflows, reentrancy bugs, transaction order dependency, etc. The former option costs a lot of money, takes time and, to the best of our knowledge, usually does not include business logic inspection, so errors in algorithms will stay. The letter option is free, rather fast but unsound and incomplete: in many cases you will get a lot of false positives, and a tool is able to detect only publicly known implementation vulnerabilities, never inspecting business logic of a contract.

In our opinion, for smart contract technology to gain mass adoption, the community needs a tool that can automatically check that smart contract implementation reflects the desired functionality, and do it in a reliable cost- and time- effective way.

In this work, we present our effort towards building such tool. We take Ethereum as a reference blockchain platform and Solidity as a reference smart contract programming language. A formal specification of a contract can be given in several forms: global invariant on state variables, properties on trace of a bounded length originating from initial state and properties on chains of events.

We use SMT-solver as a back-end to find counter-examples of a given property. To make model-checking problem tractable, we consider only a subset of Solidity language without cycles, recursion and dynamic memory management. In order to evaluate the approach in practice, we conduct a case study: we verify several functional properties of MiniDAO smart contract, a young brother of infamous TheDAO. In a few seconds our Proof-of-Concept finds violation of some non-trivial temporal property illuminating an error in a logic of the contract. To the best of our knowledge, such inspection is out of rich for existing automated tools.

1.0.1 Main Contributions

• •

We formulate 4 classes of properties suitable for formal specification of smart contract behaviour, including temporal behaviour.

• •

A subset of Solidity programming language called Sol is described. The subset is picked out with a purpose to make formal analysis easier.

• •

A procedure of encoding Sol program and its formal specification into appropriate SMT formula is described.

• •

A Proof-of-Concept demonstrating feasibility of proposed approach is implemented. Evaluation results are presented.

Symbolic model-checking is a well-known method for verifying temporal properties of reactive systems on a bounded model. However, as far as we concerned, this work is among the first that applies this general method to smart contracts verification. Moreover, we have not seen any attempts to introduce classes of properties suitable for describing functional specifications for this type of systems. Hopefully, our work partially fills this gap. Results of implemented Proof-of-Concept convince us that the approach is viable and deserves a more thorough research.

2 Ethereum Smart Contracts

In this work we propose a method for verifying Ethereum smart contract properties. We assume that contracts are programmed in a subset of Solidity programming language. Due to lack of space, we omit an introduction into the platform and the language. We advise to read [4] for such introduction.

2.0.1 Sol language.

To make a model-checking procedure tractable in practice, we picked out a subset of Solidity language that is rich enough to express interesting business logic without producing astronomical number of intermediate states.

Our small investigation into a typical program structure of a Solidity smart contract shows that from 27341 publicly available smart contracts 222https://etherscan.io/contractsVerified, July, 2018, only 23% uses any form of iteration and 26% uses dynamic array structures. However, it is well known that those programming constructs are among the most difficult ones when it comes to model-checking, so we excluded them from our scope for now.

Solidity language has a mapping data type which gives an ability to find an element without iterating through a collection. This data type partially reduces the dependency on cycles and recursion. It is interesting to note that one of the most cited smart-contracts, TheDAO [10], uses no cycles or recursion in its implementation.

2.0.2 Sol vs. Solidity.

1. for, do/while, recursion constructs are forbidden 2) no dynamic memory management support 3) only static arrays 4) var keyword is forbidden 5) only 1 smart contract is allowed to be defined 6) events are allowed to use no more than 4 arguments 7) address datatype is given by a finite set of values 8) calling other contract’s methods is not allowed; dynamic smart contract creation is also forbidden. 9) bitwise and string both datatype and operations are not supported at the moment

3 System Model

We assume that there is only one smart contract and a finite set of users performs transactions into that contract. This approximation is good enough for most practical use-cases.

Let $N_{256}=\{0\,...\,2^{256}-1\}$, $Addr=\{a_{0}\,...\,a_{n}\}$. Lets suppose that every contract state variable has an associated unique natural number. We denote a set of all possible variable values as $Val$. Let $\Phi$ denote a set of public functions of a contract, $E$ denote a set of events. Lets encode a system state as a triple: $\sigma=\langle\sigma_{c},b,t\rangle$, where $\sigma_{c}$ is a contract state, $b:Addr\rightarrow N_{256}$ is a balances of blockchain addresses, $t:N_{256}$ is a time of last block related to the smart contract. We denote a set of all possible system states as $\Sigma$, so $\sigma\in\Sigma$. We define smart-contract state as $\sigma_{c}=\langle\sigma_{cs},alive,eventlog\rangle$, where $\sigma_{cs}:\mathbb{N}\rightarrow Val$ denotes the current state of contract variables, $alive:\{True,False\}$ indicates if a contract is active or has been deleted, $eventlog:\{0\}\cup E$ denotes an event, generated by a contract during execution of last transaction, or absence of thereof.

Note that a function in Solidity is able to emit several events per transaction, and all of them will get into transaction log, but we intentionally limit our model to only one event per transaction, because, on one hand, it makes the model conceptually simpler, on the other, any finite chain of events can be encoded into some unique single event, so this restriction is not fundamental.

Let us clarify the nature of variable $t$. Transactions in Ethereum are executed by mining nodes not in FIFO order as one could imagine, but in blocks of limited size. When block is full and ready to be processed, the node starts executing transactions within that block in some unspecified order. A timestamp is assigned to each new block upon its creation and is called $blocktime$. This value is monotonically increasing and is used a source of relative time in business logic. It can be read from Solidity program using $now()$ function call. So the value of $t$ refers to the value of $blocktime$.

Let us clarify a structure of set $\Phi$. In Solidity, a function definition consists of function name, function arguments, modifiers, return type and a function body. Modifiers can specify visibility (external, public, etc) and also specify if a function is allowed to accept cryptocurrency payments together with a function call. Taking it into consideration, for each function

[TABLE]

we construct a function $f_{i}^{\prime}(\sigma_{i},v,s,t,p)$, where $\sigma_{i}\in\Sigma$ is a system state in the moment of a function call, $v\in N_{256}$ is an amount of cryptocurrency sent together with a call, $s\in Addr$ is a transaction sender address, $t\in N_{256}$ is a blocktime of a block that includes the transaction with that function call, $p=(arg_{0},arg_{1},...,arg_{n})\in\Pi$ is a tuple consisting of function formal arguments, so $\Phi=\bigcup\limits_{i=1}^{n}\{f^{\prime}_{i}\}$. The function body of $f^{\prime}$ is generated from body of $f$ by making a series of substitutions: we substitute $now()$ for $t$, $msg.sender$ for $s$, $msg.value$ for $v$, and so on. We also change the return value of a function: instead of returning a value of type T, a function $f^{\prime}_{i}$ returns a new system state $\sigma_{i+1}$. The returning value is omitted for now, as it is rearly used by external agents in practice, because it is rather difficult to monitor it. A mechanism of events is usually used instead.

We shall define several notions that let us model a system executing a smart-contract in time.

Definition 1

(Initial states). A set of initial states is defined as follows:

$I=\{\{\sigma_{c}^{0},b_{0},t_{0}\}\,|\,b_{0}:Addr\rightarrow N_{256},t_{0}\in N_{256}\},\sigma_{c}^{0}=\{\sigma_{cs}^{0},True,0\}$, where $b_{0}$ is a map between addresses and balances, $t_{0}$ denotes the blocktime of a block where the contract has been created, $\sigma_{cs}^{0}$ is a contract state right after a successful constructor call.

In Sol, it is prohibited to use any expressions that can lead to exceptions inside a constructor, along with $transfer$ and $selfdestruct$ function calls. That is why we assume that a constructor call is always successful, and its side effect is expressed solely as assignments of values to variables of the contract.

Definition 2

(Trace). Any finite sequence of system states $\sigma=\sigma_{0}\sigma_{1}...\sigma_{k-1}$ , $\sigma_{i}\in\Sigma$ is called a trace iff the following holds:

[TABLE]

where $\delta(\sigma_{i},\sigma_{i+1})$ is called a step relation (defined below), $\sigma_{0}\in I$, $len(\sigma)$ denotes a sequence length.

We denote a set of all possible state sequences (not only traces) as $2^{\Sigma}$.

Generally, a smart contract can transition into several different states from its current state because it is not known in advance what function with what parameter values and from what user address will be called. Smart contract is a highly non deterministic system reactive system. That is why when we reason about a contract we need to reason about all possible traces of that contract, not to loose interesting states that can contain an error.

Definition 3

(Behaviour). Let $\Sigma^{*}\triangleq\{\sigma\,|\,\sigma\in 2^{\Sigma}\wedge trace(\sigma)\}$ is a set of all system traces. We call $\Sigma^{*}$ a behaviour of a system.

We are allowed to put $\sigma_{i+1}$ after $\sigma_{i}$ only if a pair $(\sigma_{i},\sigma_{i+1})$ is in a special relation that we call a step relation. To define this relation, we need to clarify what exactly smart contract transaction does.

3.0.1 Partial functions.

Generally speaking, a function $f^{\prime}\in\Phi$ is not total: its execution can lead to a phenomena called an exception. Exception is an interruption of a function execution due to executing some forbidden or undefined operations. Exceptions result in a complete side-effect rollback, including cryptocurrency transfers, changing variable values, etc. Functions that can lead to exceptions are called partial, because they are defined only on a subset of all possible values of its arguments and external parameters. We could completely ignore this phenomena by making the $\delta(\sigma_{i},\sigma_{i+1})$ relation a reflexive one. But, in this case, we would get a huge amount of garbage transitions that do not lead to new states. This would greatly reduce an efficiency of symbolic model-checking procedure. To exclude such transitions we introduce a notion of function precondition.

Definition 4

(Function precondition). A precondition of a function

$f^{\prime}(\sigma_{i},v,s,t,p)\in\Phi$ is a predicate $f_{pre}(\sigma,v,s,t,p)$ such that if the predicate holds for some $\sigma\in\Sigma,v\in N_{256},s\in Addr,t\in N_{256},p\in\Pi$ then $f^{\prime}\in\Phi$ is defined on those arguments. If we equip every public function with such predicate, we get $\Phi_{pre}=\{(f^{\prime},f_{pre})\}$

Definition 5

(Step relation). It is possible to make a step from a state $\sigma_{i}$ into a state $\sigma_{i+1}$ if there exist a set of arguments $v,s,t,p$ such that at least one function $f^{\prime}\in\Phi$ is defined on those arguments $\sigma_{i},v,s,t,p$. A set of all such pairs of states we call a step relation:

[TABLE]

For convenience, we define $\delta(\sigma_{i},\sigma_{j})=((\sigma_{i},\sigma_{j})\in\Delta)$.

4 Verification problem

To this point, we have defined a model of interaction between user and a smart-contract. Lets define a problem we are aiming to solve.

Definition 6

(Verification problem). Assume $P:\Sigma^{*}\rightarrow\mathbb{B}$ is a predicate over a trace. We have to show, that $\forall\,\sigma\in\Sigma^{*}\,.\,\sigma\models P$ that is to show that a behaviour of a contract obeys $P$. We call $P$ a formal specification in this context.

Depending on a type of functional property, predicate $P$ can take a single state (trace of length 0) $P:\Sigma\rightarrow\mathbb{B}$ or a trace of fixed length $P:\Sigma_{k}^{*}\rightarrow\mathbb{B}$ as its argument. We define $\Sigma_{k}^{*}=\{\sigma\in\Sigma^{*}\,|\,len(\sigma)\leq k\}$, where $len(\sigma)$ is a length of a state sequence.

Lets define several types of functional properties we would like to be able to check.

Definition 7

(Invariant). A predicate $P:\Sigma\rightarrow\mathbb{B}$ is called an invariant iff

[TABLE]

Definition 8

(Trace property of length k). A predicate $P:\Sigma\rightarrow\mathbb{B}$ is called a trace property of length k iff

[TABLE]

We introduce another class of properties that we call events chaining properties. Properties of this type are given by a predicate over a trace of length $k$, so $P:\Sigma_{k}^{*}\rightarrow\mathbb{B}$. We shall define one instance of this property class, others can be defined similarly. We could not generalize our definition to a greater extent at this point.

Definition 9

(Events chaining) If, during an execution, an event

$E_{1}$ has occurred and $E_{2}$ has occurred afterwards, then there must be no event $E_{3}$ emitted in between, i.e.

[TABLE]

[TABLE]

Extra dependencies between event arguments $p_{0},...,p_{i};m_{0},...,m_{j};n_{0},...,n_{k}$ and arguments of a function being called $\sigma,v,s,t,p$ must be given as an extra predicate conjuncted with the one defined above.

The following class of properties express the idea that between events $E_{1}$ and $E_{2}$ is it always possible (or impossible) to perform a function call into the smart contract with a given arguments. We call this class of properties as function call possibility. As in the previous case, only one instance of such property class is given.

Definition 10

(Function call possibility) Let $P:\Sigma_{k}^{*}\rightarrow\mathbb{B}$. If an event $E_{1}$ has occured and $E_{2}$ has occurred afterwards, then it must be the case that a function call $f^{\prime}(\sigma,v,s,t,p)$ must be successful at any state between them.

[TABLE]

[TABLE]

5 Model Construction

To construct a model of a contract means to be build such tuple:

$(\Phi_{pre},E,Addr,I,k,\Sigma_{k}^{*},P)$, where $k$ denotes a path length. Lets briefly discuss how each of those elements are being built for a given smart-contract.

Set Addr.

Ethereum has $2^{160}$ distinct addresses available to be used, but for symbolic model-checking such set would be unmanageable: its size influences a number of ways a transition can be made from one state into another. That’s why we try to choose optimal set $\{a_{0},...,a_{n}\}$ such that it enables most principal scenarios of smart contract to be modeled. This choice is not automated in any way at this point, by default it is set to $Addr=\{noAddr,addr_{0},addr_{1},addr_{2},contractAddr\}$. The element $noAddr$ denotes ’undefined’ address value, a thing that is usually coded as $address(0)$ in Solidity. The element $contractAddr$ denotes an address of the contract being executed.

Set $\Phi_{pre}$.

This set is being built automatically: for every public function $f^{\prime}$ of smart contract (except a constructor), we build $f_{pre}(\sigma,v,s,t,p)$. It is done by symbolically executing a function $f^{\prime}$ and building a set of constraints that do not allow $f^{\prime}$ to throw an exception. All function calls to other internal functions are preprocessed by inserting a function body into the function $f^{\prime}$.

A list of expressions that are able to throw an exception is: division operator; reminder; mulmod; addmod; transer; assert, require, revert functions; throw; calling non-payable functions with $v>0$; a situation when $s=contractAddr$; trying to execute a function of a deleted smart contract, i.e. $\sigma_{cs}[alive]=False$.

There are no cycles and recursion available in Sol language, that’s why we are guaranteed for this symbolic execution procedure to terminate.

Set $E$.

This set is being built automatically from events defined in the smart contract. Events that are not used will be omitted.

Set $I$.

A set of initial states. The set is being built automatically by evaluating a constructor of the smart contract.

Value $k$.

The value denotes an exact length of a trace. It is given explicitly by the user. If a property being checked is an invariant,then this parameter is ignored.

Set $\Sigma_{k}^{*}$.

The set is constructed implicitly, by giving a system of contraints over a set of system states $\sigma_{[0...k-1]}$ and a set of parameters $(v,s,t,p)$, where i-th tuple of parameters corresponds to the i-th function call. Lets define a transition relation as follows:

[TABLE]

Definition 11

(Path). Lets define a path between states as follows:

[TABLE]

The difference between a path and a trace is in the originating state: in the former, it is allowed to be any state, not only initial. A path of length zero consists of only one state, and has no transitions.

Let us introduce a time monotonicity requirement: $T=\bigwedge\limits_{i=0}^{k-1}{t_{i}<t_{i+1}}$, and a restriction on originating addresses:

[TABLE]

and a requirement for initial state origin: $I(\sigma_{0})$. In this case, a predicate

$I(\sigma_{0})\wedge T\wedge NoSelfAddrCall\wedge path(\sigma_{[0..k-1]})$ describes a transition system of our smart contract executing all possible $k$ consecutive transactions. Finding the right assignments for variables $\sigma_{[0..k-1]}$ and $(v,s,t,p)$ of this formula inside an SMT-solver implicitly generates the set $\Sigma_{k}^{*}$.

Predicate $P$

. The predicate is given by the user and describes formal specification for the contract.

Thereby, it is possible to automatically extract a model from a Sol program that can be checked using an SMT-solver. A user has to specify a functional specification $P$, trace length $k$ and the number of distinct addresses in the set $Addr$.

6 Verification algorithms

Here, we describe algorithms that check aforementioned classes of properties. Let $P(\sigma)$ denote a property we would like to check. The expression $SAT(e,Vars)$ means that $e$ is checked by SAT/SMT solver for satisfiability, i.e. a solver look for values for variables of $Vars$ such that expression $e$ evaluates to $True$. If such assignment is found then the expression returns $True$, otherwise $False$. A result $unknown$ is not concerned here because we stay inside decidable theories, and for such theories this answer simply means that a solver ran out of time. A predicate $path(\sigma_{[0..n]})$ is defined the same as above. Each algorithm returns $True$ if property $P(\sigma)$ holds, otherwise $False$ is returned.

In the pseudo-code, the expression $Vars=\{p_{i}:t_{i}\}$ means that for every variable $p$ we add corresponding proposition variable of type $t$ or an array of variables into solver’s context.

Some of those algorithms were published in the past. The model-checking procedure for paths of length $k$ was thoroughly described in different variations in [16]. The invariant proving algorithm is considered to be well known also. However, to make the work self-sufficient, we include pseudo-code for those algorithms also.

7 Proof Of Concept

In order to evaluate described algorithms, we have programmed the MiniDAO smart-contract, a simpler version of infamous TheDAO, and tried to find a counter-example of several specified requirements. The MiniDAO is programmed using Sol programming language, and functional properties are encoded in a first-order logic predicate form. Both artefacts (source code and requirements) were manually translated into the language of SMT-solver and model-checked, making time measurements for different properties using different model parameters. We briefly describe the purpose of this contract and some desired functional properties that we later use as a partial functional specification.

7.1 MiniDAO Smart Contract

MiniDAO is a smart contract that implements an autonomous investment fund. There are two types of users in the fund: investors and contractors. Investor is a user that deposits his money into the fund and later votes for or against a contractor’s proposal. Contractor is a user that makes a proposal of some new project and, if enough funds are raised, implements this project. It is assumed that the invested sum and dividends are paid back to investors later using smart contract facility, but this functionality is not implemented right now.

An interface of the MiniDAO is given on . The full listing is available at 333https://bitbucket.org/unboxed_type/minidao/src/master/contracts/MiniDAO.sol

To give investor an ability to get back his invested funds, the refund method is implemented. Refund is made only if the investor has not voted for any proposal. Investors are able to transfer their tokens to other investors using now standard ERC20 token interface functions.

Suppose that we are interested in engaging as many investors as possible in our MiniDAO fund. To minimize investors fear of money loss, we claim the following: ”If you do not vote for any proposal, you will always be able to refund your deposit”. To prove our assertion, we show the code of the refund function.

The function looks simple and convincing. Yet, our assertion does not hold.

7.1.1 Majority Attack

Lets discuss a possible attack scenario. Suppose that two investors have invested crypto currency equal to X and Y MiniDAO tokens respectively. After that, the third investor comes in and invests amount equal to $2\times(X+Y)$ tokens. That third investor now has a majority of votes ($2/3\approx 66\%$) when decision is to be made about project funding. It is not prohibited for an investor to be a contractor also, this gives an opportunity for that investor to register his own proposal with expected amount of as much as $3\times(X+Y)$ tokens. After that, because his vote is final, he votes for his own proposal and calls execute_proposal. All funds of MiniDAO are transferred to that third intruder investor leaving two other investors with nothing. We have an obvious violation of the aforementioned property: investors did not vote, but refund is now impossible for them.

The Majority Attack is described in the TheDAO whitepaper [10]. Lets suppose we do not know about this attack and would like to ask our verification tool to check the refund property automatically.

7.2 MiniDAO Functional Requirements

We give a partial functional specification by formulating 3 properties that we will later check.

7.2.1 NotVotedRefund Property.

If some investor with the address $inv$ deposited some amount of money and not voted for any proposal afterwards, then he will always be able to get a refund by calling the refund function.

[TABLE]

7.2.2 InvDaoBalance Property.

In any reachable state, the sum of MiniDAO token balances is equal to the total amount of emitted tokens, i.e.

[TABLE]

7.2.3 RejectedNotExecuted Property

. A rejected proposal must not receive any funds from the MiniDAO.

[TABLE]

7.3 Finding Errors in MiniDAO

As we discussed earlier, to construct a model means to construct a number of objects $(\Phi_{pre},E,Addr,I,k,\Sigma_{k}^{*},P)$. After that we can run one of verification algorithms given in section 6. The tool that we are building will construct those objects automatically except $Addr$, $k$ and $P$. While it is not ready, we constructed those objects manually. We translated MiniDAO source code together with its specifications into the language of SMT-solver.

After this translation and some further optimizations, we received a model that produced a counter-example for two out of three properties during model-checking.

NotVotedRefund property.

The counter-example 1 is represented as a chain of occurred events. The first NoEvent event denotes the initial state. The investor with address $addr4$ is not able to refund after event 5. We did not fix this error in any way.

InvDaoBalance property.

This property was also violated. In the first version of MiniDAO, the method $vote$ was wrongly settings the balance of investor to zero after the vote. The error was fixed and checked again. After the fix, no counter-example was found.

RejectedNotExecuted property.

The check was successful, there was no trace found that violated this property.

8 Efficiency Evaluation

We tried our proof-of-concept for different set sizes and path length, measuring the time needed to find a counter-example or prove the absence of thereof; results are presented in the table 2 below.

Keep in mind that those results give only very rough presentation of the model-checking efficiency for such systems because SAT/SMT-solvers are known to be very sensitive to any changes in the model or in the solver’s parameters.

Experiments were conducted using Intel Core i7-4770 4 cores 3.4GHz CPU, 32 GB RAM running Linux Ubuntu 18.04.1 LTS 64-bit OS virtual machine using VirtualBox 5.1.24 hypervisor on Windows 7 OS. We have used Z3 SMT-solver ver. 4.8.2 64 bit, the model is written using Z3Py binding for Python.

9 Related Works

A lot of research is being done in the area of smart contracts reliability, just to name a few [5][6] [8][15] [12][11] [9][13].

In [5], authors present a thorough list of known Solidity language and Ethereum Virtual Machine vulnerabilities. TheDAO attack scenario is described in details.

In [6], authors propose a way to prove the absence of several kinds of typical implementation errors by encoding Solidity* program info F* language together with some specially crafted abstract data types that help track error codes management.

In [15], authors investigate ways to program Ethereum smart contracts using Idris functional language; by using its powerful type system, authors propose several algebraic types that help eliminate typical implementation errors during a compilation stage. The back-end that translates Idris into EVM bytecode is also presented.

Works [12] [13] describe tools for Solidity smart contract static analysis called Oyente and Mythrill accordingly. Tools are based on symbolic execution technique and aim to find a series of conditions that, when met, will result in executing potentially harmful programming constructs.

In [11], a tool called ZEUS is presented. This tool can find a scenarios of deviation from user-specified policies. Policies are written in a language of assertions about smart-contract state variables with basic arithmetic support. In this respect, ZEUS is the closest tool to ours in that it makes an effort to analyse business logic against specification stated in a form of policies. Unfortunately, ZEUS is not able to analyse temporal properties, and is aiming to check only state properties.

The work [9] is among the first that proposed using a theorem prover environment to formally verify properties of a smart-contract. The author encoded EVM instructions semantics in Coq and later in Isabelle. Using this framework, a developer is able to prove properties of his smart-contracts on the bytecode level inside a theorem prover. Being the most foundational among all other approaches, this method gives the highest guarantees on correctness of producing artefacts, but potentially takes a lot of time and effort.

One more step in similar direction is [17]. In this work, an effort towards formalizing a subset of Solidity language semantics inside a theorem prover is described.

10 Conclusion and Future Work

In this work, we described a conceptual device of symbolic model-checker for Solidity smart-contracts based on SMT-solver, that is able to detect deviations from prescribed behaviour on traces of the given length, or breaking an invariant.

While the model-checking tool itself is under construction, the viability of the proposed method was evaluated on the MiniDAO smart-contract, a weak analogy of TheDAO. Results convinces us that proposed method is indeed practical and needs further investigation. For the future work, we would like to mention the following directions:

• •

The specification language need not be as complicated as first order logic language, which is quite verbose and a bit alien to many developers. We need to develop an alternative way of encoding behaviour of a smart-contract. Different flavours of temporal logic do not answer this question in our opinion.

• •

SMT-solvers are very sensitive to a model representation. Optimality of such representation influences on how fast the model-checking process will execute. Thus, we need to develop optimization strategies for representing Solidity datatypes and code when expressed in SMT solver language.