See discussions, stats, and author profiles for this publication at: https://www.researchgate.

net/publication/329387888

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

Preprint · December 2018

DOI: 10.48550/arXiv.1812.00619

CITATIONS READS
0 296

1 author:

Evgeniy Shishkin
JSC "InfoTeCS", Russia, Moscow
7 PUBLICATIONS 27 CITATIONS

SEE PROFILE

All content following this page was uploaded by Evgeniy Shishkin on 04 March 2019.

The user has requested enhancement of the downloaded file.

 Debugging Smart Contract’s Business Logic
Using Symbolic Model Checking

Evgeniy Shishkin

InfoTeCS, Advanced Research Department

arXiv:1812.00619v1 [cs.LO] 3 Dec 2018

Stariy Petrovsko-Razumovskiy Proezd 1/23 bld.1, Moscow, Russia

[email protected]

Abstract. Smart contracts are a special type of programs running inside

a blockchain. Immutable and transparent, they provide means to imple-
ment 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 auto-
mated 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 lat-
ter 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.

Keywords: Symbolic Model-Checking; Smart Contracts; Formal Spec-

ification

1 Introduction
In 2008, Satoshi Nakamoto 1 published a paper where he described an architec-
ture 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 mas-
sive 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.
1
This is a pseudoname. Real name of this crypto enthusiast is still unknown.
2 Evgeniy Shishkin

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 knowl-
edge, 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 im-
plementation 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 prop-
erty. 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 in-
famous 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.
Debugging Smart Contract’s Business Logic Using Symbolic Model Checking 3

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 sub-
set is picked out with a purpose to make formal analysis easier.
– A procedure of encoding Sol program and its formal specification into ap-
propriate SMT formula is described.
– A Proof-of-Concept demonstrating feasibility of proposed approach is imple-
mented. Evaluation results are presented.

Symbolic model-checking is a well-known method for verifying temporal prop-

erties 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 sys-
tems. 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 proper-
ties. We assume that contracts are programmed in a subset of Solidity program-
ming language. Due to lack of space, we omit an introduction into the platform
and the language. We advise to read [4] for such introduction.

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 2 , 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
https://etherscan.io/contractsVerified, July, 2018
4 Evgeniy Shishkin

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 N256 = {0 ... 2256 − 1}, Addr = {a0 ... an }. Lets suppose that every con-
tract state variable has an associated unique natural number. We denote a set
of all possible variable values as V al. Let Φ denote a set of public functions of
a contract, E denote a set of events. Lets encode a system state as a triple:
σ = hσc , b, ti, where σc is a contract state, b : Addr → N256 is a balances of
blockchain addresses, t : N256 is a time of last block related to the smart con-
tract. We denote a set of all possible system states as Σ, so σ ∈ Σ. We define
smart-contract state as σc = hσcs , alive, eventlogi, where σcs : N → V al denotes
the current state of contract variables, alive : {T rue, F alse} indicates if a con-
tract is active or has been deleted, eventlog : {0}∪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 exe-
cuted 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 exe-
cuting 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 Φ. 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

f unction fi (arg0 , arg1 , ..., argn ) public [payable] [return(T )]

Debugging Smart Contract’s Business Logic Using Symbolic Model Checking 5

we construct a function fi′ (σi , v, s, t, p), where σi ∈ Σ is a system state in the

moment of a function call, v ∈ N256 is an amount of cryptocurrency sent to-
gether with a call, s ∈ Addr is a transaction sender address, t ∈ N256 is
a blocktime of a block that includes the transaction with that function call,
p = (arg0 , arg1 , ..., argn ) ∈ Π is a tuple consisting of function formal argu-
Sn
ments, so Φ = {fi′ }. The function body of f ′ is generated from body of f
i=1
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 fi′ returns a new system state
σ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 = {{σc0 , b0 , t0 } | b0 : Addr → N256 , t0 ∈ N256 }, σc0 = {σcs
0
, T rue, 0}, where
b0 is a map between addresses and balances, t0 denotes the blocktime of a block
0
where the contract has been created, σcs 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 transf er and self destruct 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 σ = σ0 σ1 ...σk−1 ,
σi ∈ Σ is called a trace iff the following holds:

trace(σ) = ∀i ∈ N, 0 ≤ i < len(σ).δ(σi , σi+1 )

where δ(σi , σi+1 ) is called a step relation (defined below), σ0 ∈ I, len(σ) denotes
a sequence length.
We denote a set of all possible state sequences (not only traces) as 2Σ .
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 Σ ∗ , {σ | σ ∈ 2Σ ∧ trace(σ)} is a set of all
system traces. We call Σ ∗ a behaviour of a system.
We are allowed to put σi+1 after σi only if a pair (σi , σ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.
6 Evgeniy Shishkin

Partial functions. Generally speaking, a function f ′ ∈ Φ is not total: its execu-

tion 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 phe-
nomena by making the δ(σi , σ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 ′ (σi , v, s, t, p) ∈ Φ is a predicate fpre (σ, v, s, t, p) such that if the predicate holds
for some σ ∈ Σ, v ∈ N256 , s ∈ Addr, t ∈ N256 , p ∈ Π then f ′ ∈ Φ is defined on
those arguments. If we equip every public function with such predicate, we get
Φpre = {(f ′ , fpre )}

Definition 5. (Step relation). It is possible to make a step from a state σi into a

state σi+1 if there exist a set of arguments v, s, t, p such that at least one function
f ′ ∈ Φ is defined on those arguments σi , v, s, t, p. A set of all such pairs of states
we call a step relation:

∆ = {(σi , σj ) : ∃(f ′ , fpre ) ∈ Φpre , v, s, t, p . σj = f ′ (σi , v, s, t, p)∧fpre (σi , v, s, t, p)}

For convenience, we define δ(σi , σj ) = ((σi , σj ) ∈ ∆).

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 : Σ ∗ → B is a predicate over

a trace. We have to show, that ∀ σ ∈ Σ ∗ . σ |= 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 : Σ → B or a trace of fixed length P : Σk∗ → B as its
argument. We define Σk∗ = {σ ∈ Σ ∗ | len(σ) ≤ k}, where len(σ) 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 : Σ → B is called an invariant iff

∀σ0 ∈ I . P (σ0 ) ∧ ∀σi , σj ∈ Σ . (δ(σi , σj ) ∧ P (σi )) → P (σj )

Debugging Smart Contract’s Business Logic Using Symbolic Model Checking 7

Definition 8. (Trace property of length k). A predicate P : Σ → B is called a

trace property of length k iff
∀ σ ∗ ∈ Σk∗ , i ∈ N . i ≤ len(σ ∗ ) → P (σi∗ )
We introduce another class of properties that we call events chaining prop-
erties. Properties of this type are given by a predicate over a trace of length k,
so P : Σk∗ → 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
E1 has occurred and E2 has occurred afterwards, then there must be no event E3
emitted in between, i.e.

P (σ ∗ ) = ∃ i, j ∈ N . σi∗ [eventlog] = E1 ∧ σj∗ [eventlog] = E2 ∧ i < j ≤ len(σ ∗ ) →

∀k ∈ N.i < k < j . σk∗ [eventlog] 6= E3
Extra dependencies between event arguments p0 , ..., pi ; m0 , ..., mj ; n0 , ..., nk and
arguments of a function being called σ, v, s, t, p must be given as an extra pred-
icate conjuncted with the one defined above.
The following class of properties express the idea that between events E1 and
E2 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 : Σk∗ → B. If an event E1 has
occured and E2 has occurred afterwards, then it must be the case that a function
call f ′ (σ, v, s, t, p) must be successful at any state between them.
P (σ ∗ ) = ∃ i, j ∈ N . σi∗ [eventlog] = E1 ∧ σj∗ [eventlog] = E2 ∧ i < j ≤ len(σ ∗ ) →
∀k ∈ N, i < k < j . fpre (σk∗ , v, s, t, p) = T rue

5 Model Construction
To construct a model of a contract means to be build such tuple:
(Φpre , E, Addr, I, k, Σ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 2160 distinct addresses available to be used, but for sym-
bolic model-checking such set would be unmanageable: its size influences a num-
ber of ways a transition can be made from one state into another. That’s why we
try to choose optimal set {a0 , ..., an } 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, addr0 , addr1 , addr2 , 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.
8 Evgeniy Shishkin

Set Φpre . This set is being built automatically: for every public function f ′ of
smart contract (except a constructor), we build fpre (σ, v, s, t, p). It is done by
symbolically executing a function f ′ and building a set of constraints that do
not allow f ′ to throw an exception. All function calls to other internal functions
are preprocessed by inserting a function body into the function f ′ .
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. σcs [alive] = F alse.
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 Σk∗ . The set is constructed implicitly, by giving a system of contraints over
a set of system states σ[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:

transition(σi , σi+1 ) =
_
|Φpre |
(fjpre (σi , vi , si , ti , pi ) = T rue ∧ σi+1 = fj′ (σi , vi , si , ti , pi ))
j=1

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

^
path(σ[0..k] ) = transition(σi , σi+1 )
0≤i<k

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.
V
k−1
Let us introduce a time monotonicity requirement: T = ti < ti+1 , and a
i=0
restriction on originating addresses:

^
k−1
N oSelf AddrCall = (si 6= contractAddr ∧ si 6= noAddr),
i=0
 Debugging Smart Contract’s Business Logic Using Symbolic Model Checking 9

and a requirement for initial state origin: I(σ0 ). In this case, a predicate
I(σ0 ) ∧ T ∧ N oSelf AddrCall ∧ path(σ[0..k−1] ) describes a transition system of
our smart contract executing all possible k consecutive transactions. Finding the
right assignments for variables σ[0..k−1] and (v, s, t, p) of this formula inside an
SMT-solver implicitly generates the set Σk∗ .

Predicate P . The predicate is given by the user and describes formal specifica-
tion 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 (σ) denote a property we would like to check. The expression SAT (e, V ars)
means that e is checked by SAT/SMT solver for satisfiability, i.e. a solver look
for values for variables of V ars such that expression e evaluates to T rue. If
such assignment is found then the expression returns T rue, otherwise F alse. 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(σ[0..n] ) is defined the same as above. Each algorithm returns
T rue if property P (σ) holds, otherwise F alse is returned.
In the pseudo-code, the expression V ars = {pi : ti } 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 al-
gorithms also.

Listing 1.1. Algorithm 1. Checking invariant property

1 Vars = {σ[0,1] : Σ,v[0,1] : N256 , s[0,1] : Addr, t[0,1] : N256 , p[0,1] : Π }
2 i f (SAT( I(σ0 ) ∧ ¬P (σ0 ), V ars) ) {
3 p r i n t s0
4 return f a l s e
5 }
6 i f (SAT( P (σ0 ) ∧ δ(σ0 , σ1 ) ∧ ¬P (σ1 )), V ars)) {
7 p r i n t f ′ , σ0 , σ1
8 return f a l s e
9 }
10 return true
 10 Evgeniy Shishkin

Listing 1.2. Algorithm 2. Checking a trace property of length k

1 Vars = {σ[0..k−1] : Σ, v[0..k−1] : N256 , s[0..k−1] : Addr, t[0..k−1] : N256 ,

2 p[0..k−1] : Π }
3 i = 0
4 w h i l e ( i < k ) do {
5 i f (SAT( I(σ0 ) ∧ path(σ[0..i] ) ∧ ¬P (σi ), V ars) ) {
6 p r i n t σ[0..i]
7 return f a l s e
8 }
9 i = i + 1
10 }
11 return true

Listing 1.3. Algorithm 3. Checking events chaining property

1 Vars = {σ[0..k−1] : Σ, v[0..k−1] : N256 , s[0..k−1] : Addr, t[0..k−1] : N256 ,

2 p[0..k−1] : Π, m, n, q : N256 }
3 i = 3
4 w h i l e ( i < k ) do {
cs
5 i f (SAT( I(σ0 ) ∧ path(σ[0..i] ) ∧ σm [eventlog] = E1 ∧ σncs [eventlog] = E2
6 ∧ (m < n) ∧ (q > m) ∧ (q < n) ∧ σqcs [eventlog] = E3 , V ars) ) {
7 p r i n t σ[0..i]
8 return f a l s e
9 }
10 i = i + 1
11 }
12 return true

Listing 1.4. Algorithm 4. Checking functional call possibility property

1 Vars = {σ[0..k−1] : Σ, v[0..k−1] : N256 , s[0..k−1] : Addr, t[0..k−1] : N256 ,

2 p[0..k−1] : Π, m, n, q : N256 }
3 i = 3
4 w h i l e ( i < k ) do {
cs
5 i f (SAT( I(σ0 ) ∧ path(σ[0..i] ) ∧ σm [eventlog] = E1 ∧ σncs [eventlog] = E2
6 ∧ (m < n) ∧ (q > m) ∧ (q < n) ∧ ¬fpre (σq , vq , sq , tq , pq ), V ars) ) {
7 p r i n t σ[0..i] , vq , sq , tq , pq
8 return f a l s e
9 }
10 i = i + 1
11 }
12 return true
Debugging Smart Contract’s Business Logic Using Symbolic Model Checking 11

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 parame-
ters. 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 3
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.
Listing 1.5. The MiniDAO interface
interface ERC20Interfa ce { /* standard definition */ }
interface MiniDAOInte rf a ce {
function deposit () public payable ;
function vote ( uint proposalId , bool supports ) public ;
function refund () public ;
function propose ( address recipient , uint amount ,
string test ) ;
function execute_pro p os al () public ;
event Voted ( address voter , uint proposalId , bool supports ) ;
event Refund ( address investor , uint tokens ) ;
event Deposited ( address investor , uint tokens ) ;
event ProposalAdded ( uint amount , uint proposalId ) ;
event ProposalExe cu t ed ( uint proposalId ) ;
event ProposalRej ec t ed ( uint proposalId ) ;
}
contract MiniDAO is MiniDAOInterface , ERC20Interfa ce {
/* Implementatio n goes here */ }

3
https://bitbucket.org/unboxed type/minidao/src/master/contracts/MiniDAO.
sol
12 Evgeniy Shishkin

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
Listing 1.6. The refund function body
simple and convinc-
function refund () public { ing. Yet, our asser-
address sender = msg . sender ; tion does not hold.
uint tokens = balance [ sender ];
require ( isVoted [0][ sender ] == false ) ;
require ( tokens > 0) ; Majority Attack
require ( DAO_tokens _ em i tt e d >= tokens ) ; Lets discuss a possi-
DAO_tokens_ e mi t te d -= tokens ; ble attack scenario.
balance [ sender ] = 0; Suppose that two
sender . transfer ( tokens * DAO_token_p ri c e ) ; investors have in-
emit Refund ( sender , tokens ) ; vested crypto cur-
} rency equal to X
and Y MiniDAO tokens respectively. After that, the third investor comes in
and invests amount equal to 2 × (X + Y ) tokens. That third investor now has
a majority of votes (2/3 ≈ 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 × (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 trans-
ferred 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 sup-
pose 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.

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.
i
N otV otedRef und(σ) = ∃i, inv, s, 1 ≤ i < k.σcs [logs] = Deposited(inv, s) ∧
j
∃j, inv1 , s1 , id, 1 ≤ j < k.σcs [logs] = P roposalAdded(inv1 , s1 , id) ∧
n
∀n, id1 , 1 ≤ n < k.σcs [logs] 6= V oted(inv, id1 , T rue) ∧
n
σcs [logs] 6= V oted(inv, id1 , F alse) ∧
n n
σcs [logs] 6= Ref und(inv) ∧ σcs [logs] 6= T ransf er(inv) →
∀m, i ≤ m < k . ref undpre (σm , v, inv, t, p)
Debugging Smart Contract’s Business Logic Using Symbolic Model Checking 13

InvDaoBalance Property. In any reachable state, the sum of MiniDAO token

balances is equal to the total amount of emitted tokens, i.e.
X
k
InvDaoBalance(σk ) = σcs [daoBalance[i]] = daoT okensEmitted
i∈Addr

RejectedNotExecuted Property . A rejected proposal must not receive any

funds from the MiniDAO.
j
RejectedN otExecuted(σ) = ∀n.∃i, j ∈ N.σcs [logs] = P roposalAdded(n, amount) ∧
j
σcs [logs] = P roposalRejected(n) ∧ i < j → ∀k, i < k < j.
k
σcs [logs] 6= P roposalExecuted(n)

7.3 Finding Errors in MiniDAO

As we discussed earlier, to construct a model means to construct a number

of objects (Φpre , E, Addr, I, k, Σ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 0. NoEvent

counter-example 1 is represented 1. Deposited ( addr4 , 2976)
2. Deposited ( addr2 , 1672)
as a chain of occurred events. The
3. ProposalAdde d ( addr4 , 4648 , 1)
first NoEvent event denotes the 4. Voted ( addr4 , 1 , 1)
initial state. The investor with ad- 5. ProposalEx ec ut e d (1)
dress addr4 is not able to refund
after event 5. We did not fix this step = 5 , investor = addr2
error in any way.
Fig. 1. The counter-example for NotVote-
InvDaoBalance property. This dRefund property.
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.
14 Evgeniy Shishkin

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.

Fig. 2. Left table: a duration of checking NotVotedRefund property. Notation > N

means that we have stopped the checking process after N seconds. Middle table: a
duration of checking RejectedNotExecuted property. Right table: a duration of checking
InvDaoBalance property. Trace length column denotes the minimal length of a trace;
the maximum trace length was set to 12 in all cases.

Trace Integer Time, Trace Integer Time, Integer Time,

length width, sec length width, sec width, sec
bits bits bits
6 16 57 6 16 14 16 637
8 16 10 8 16 11 24 478
12 16 971 12 16 1.6 - -
6 32 47 6 32 48 - -
8 32 171 8 32 35 - -
12 32 > 2500 12 32 5 - -

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 man-
agement.
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.
Debugging Smart Contract’s Business Logic Using Symbolic Model Checking 15

Works [12] [13] describe tools for Solidity smart contract static analysis called
Oyente and Mythrill accordingly. Tools are based on symbolic execution tech-
nique and aim to find a series of conditions that, when met, will result in exe-
cuting 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 asser-
tions 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 envi-
ronment 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 ap-
proaches, 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 lan-
guage, 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. Dif-
ferent 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 exe-
cute. Thus, we need to develop optimization strategies for representing So-
lidity datatypes and code when expressed in SMT solver language.

References
1. The multi-sig hack: A postmortem. https://paritytech.io/the-multi-sig-
hack-a-postmortem/, accessed: 2018-11-14
 16 Evgeniy Shishkin

2. The parity hack. https://www.crowdfundinsider.com/2017/11/124200-

ethereum-parity-hack-may-impact-eth-500000-146-million/, accessed:
2018-11-14
3. Smart contracts and the dao implosion. https://www.multichain.com/blog/2016/
06/smart-contracts-the-dao-implosion/, accessed: 2018-11-14
4. Solidity programming language documentation, 2018. https://solidity.
readthedocs.io/en/v0.4.24/ (2018)
5. Atzei, N., Bartoletti, M., Cimoli, T.: A survey of attacks on ethereum smart con-
tracts (sok). In: International Conference on Principles of Security and Trust. pp.
164–186. Springer (2017)
6. Bhargavan, K., Delignat-Lavaud, A., Fournet, C., Gollamudi, A., Gonthier, G.,
Kobeissi, N., Kulatova, N., Rastogi, A., Sibut-Pinote, T., Swamy, N., et al.: Formal
verification of smart contracts: Short paper. In: Proceedings of the 2016 ACM
Workshop on Programming Languages and Analysis for Security. pp. 91–96. ACM
(2016)
7. Buterin, V., et al.: Ethereum white paper, 2014. https://github.com/ethereum/
wiki/wiki/White-Paper (2013)
8. Delmolino, K., Arnett, M., Kosba, A., Miller, A., Shi, E.: Step by step towards
creating a safe smart contract: Lessons and insights from a cryptocurrency lab. In:
International Conference on Financial Cryptography and Data Security. pp. 79–94.
Springer (2016)
9. Hirai, Y.: Defining the ethereum virtual machine for interactive theorem provers.
In: International Conference on Financial Cryptography and Data Security. pp.
520–535. Springer (2017)
10. Jentzsch, C.: Decentralized autonomous organization to automate governance.
White paper, November (2016)
11. Kalra, S., Goel, S., Dhawan, M., Sharma, S.: Zeus: Analyzing safety of smart
contracts. NDSS (2018)
12. Luu, L., Chu, D.H., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts
smarter. In: Proceedings of the 2016 ACM SIGSAC Conference on Computer and
Communications Security. pp. 254–269. ACM (2016)
13. Mueller, B.: Smashing ethereum smart contracts for fun and real profit. HITB
SECCONF Amsterdam (2018)
14. Nakamoto, S.: Bitcoin: A peer-to-peer electronic cash system (2008)
15. Pettersson, J., Edström, R.: Safer smart contracts through type-driven develop-
ment. Master’s thesis, Dept. of CS&E, Chalmers University of Technology & Uni-
versity of Gothenburg, Sweden (2015)
16. Sheeran, M., Singh, S., Stålmarck, G.: Checking safety properties using induction
and a sat-solver. In: International conference on formal methods in computer-aided
design. pp. 127–144. Springer (2000)
17. Zakrzewski, J.: Towards verification of ethereum smart contracts: a formalization
of core of solidity [preprint], 2018. https://www.mimuw.edu.pl/~jz321207/papers/
vstte18-solidity.pdf (2018)

View publication stats