Making Smart Contracts Smarter

Loi Luu Duc-Hiep Chu Hrishi Olickel

National University of Singapore National University of Singapore Yale-NUS College
loiluu@comp.nus.edu.sg hiepcd@comp.nus.edu.sg hrishi.olickel@yale-nus.edu.sg
Prateek Saxena Aquinas Hobor
National University of Singapore Yale-NUS College&
prateeks@comp.nus.edu.sg National University of Singapore
hobor@comp.nus.edu.sg

ABSTRACT been used more broadly [2–4]. One prominent new use for
Cryptocurrencies record transactions in a decentralized data blockchains is to enable smart contracts.
structure called a blockchain. Two of the most popular A smart contract is a program that runs on the blockchain
cryptocurrencies, Bitcoin and Ethereum, support the fea- and has its correct execution enforced by the consensus pro-
ture to encode rules or scripts for processing transactions. tocol [5]. A contract can encode any set of rules represented
This feature has evolved to give practical shape to the ideas in its programming language—for instance, a contract can
of smart contracts, or full-fledged programs that are run on execute transfers when certain events happen (e.g. pay-
blockchains. Recently, Ethereum’s smart contract system ment of security deposits in an escrow system). Accordingly,
has seen steady adoption, supporting tens of thousands of smart contracts can implement a wide range of applications,
contracts, holding millions dollars worth of virtual coins. including financial instruments (e.g., sub-currencies, finan-
In this paper, we investigate the security of running smart cial derivatives, savings wallets, wills) and self-enforcing or
contracts based on Ethereum in an open distributed network autonomous governance applications (e.g., outsourced com-
like those of cryptocurrencies. We introduce several new se- putation [6], decentralized gambling [7]).
curity problems in which an adversary can manipulate smart A smart contract is identified by an address (a 160-bit
contract execution to gain profit. These bugs suggest subtle identifier) and its code resides on the blockchain. Users in-
gaps in the understanding of the distributed semantics of the voke a smart contract in present cryptocurrencies by sending
underlying platform. As a refinement, we propose ways to transactions to the contract address. Specifically, if a new
enhance the operational semantics of Ethereum to make con- transaction is accepted by the blockchain and has a con-
tracts less vulnerable. For developers writing contracts for tract address as the recipient, then all participants on the
the existing Ethereum system, we build a symbolic execution mining network execute the contract code with the current
tool called Oyente to find potential security bugs. Among state of the blockchain and the transaction payloads as in-
19, 366 existing Ethereum contracts, Oyente flags 8, 833 of puts. The network then agrees on the output and the next
them as vulnerable, including the TheDAO bug which led state of the contract by participating in a consensus proto-
to a 60 million US dollar loss in June 2016. We also discuss col. Ethereum, a more recent cryptocurrency, is a promi-
the severity of other attacks for several case studies which nent Turing-complete smart contract platform [2]. Unlike
have source code available and confirm the attacks (which Bitcoin, Ethereum supports stateful contracts in which val-
target only our accounts) in the main Ethereum network. ues can persist on the blockchain to be used in multiple
invocations. In the last six months alone, roughly 15, 000
smart contracts have been deployed in the Ethereum net-
1. INTRODUCTION work, suggesting a steady growth in the usage of the plat-
Decentralized cryptocurrencies have gained considerable form (see Figure 1). As Ethereum receives more public expo-
interest and adoption since Bitcoin was introduced in 2009 [1]. sure and other similar projects like Rootstock [8] and Coun-
At a high level, cryptocurrencies are administered publicly terParty [9] emerge on top of the Bitcoin blockchain, we
by users in their network without relying on any trusted expect the number of smart contracts to grow.
parties. Users in a cryptocurrency network run a consen- Security problems in smart contracts. Smart contracts
sus protocol to maintain and secure a shared ledger of data can handle large numbers of virtual coins worth hundreds of
(the blockchain). Blockchains were initially introduced for dollars apiece, easily making financial incentives high enough
peer-to-peer Bitcoin payments [1], but more recently, it has to attract adversaries. Unlike traditional distributed appli-
cation platforms, smart contract platforms such as Ethereum
Permission to make digital or hard copies of all or part of this work for personal or
classroom use is granted without fee provided that copies are not made or distributed operate in open (or permissionless) networks into which arbi-
for profit or commercial advantage and that copies bear this notice and the full citation trary participants can join. Thus, their execution is vulner-
on the first page. Copyrights for components of this work owned by others than the able to attempted manipulation by arbitrary adversaries—
author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or
republish, to post on servers or to redistribute to lists, requires prior specific permission a threat that is restricted to accidental failures in tradi-
and/or a fee. Request permissions from permissions@acm.org. tional permissioned networks such as centralized cloud ser-
CCS’16, October 24 - 28, 2016, Vienna, Austria vices [10, 11]. Although users in Ethereum have to follow a
c 2016 Copyright held by the owner/author(s). Publication rights licensed to ACM. predefined protocol when participating in the network, we
ISBN 978-1-4503-4139-4/16/10. . . $15.00 show that there is considerable room for manipulation of
DOI: http://dx.doi.org/10.1145/2976749.2978309

254
 20000 risk of not seeing real deployment. If such a requirement
is unacceptable, we provide a tool called Oyente for users

Number of smart contracts

15000 to detect bugs in as a pre-deployment mitigation. Oyente
is a symbolic execution tool exclusively designed to analyze
Ethereum smart contracts. It follows the execution model
10000
of Ethereum smart contracts [15] and directly works with
Ethereum virtual machine (EVM) byte code without ac-
5000 cess to the high level representation (e.g., Solidity [16], Ser-
pent [17]). This design choice is vital because the Ethereum
0
blockchain only stores the EVM byte code of contracts, not
their source. Oyente is open source and will be available
5 5 5 5 5 5 5 6 6 6 6 6 6 6
01 01 01 01 01 01 01 01 01 01 01 01 01 01
.2 .2 .2 .2 .2 .2 .2 .2 .2 .2 .2 .2 .2 .2 for public use soon from our project page [18].
. 08 .09 .10 .10 .11 .12 .12 .01 .02 .02 .03 .03 .04 .05
25 15 06 25 14 04 24 13 02 21 12 29 15 03 Evaluation. We ran Oyente on 19, 366 smart contracts
Date from the first 1, 460, 000 blocks in Ethereum network and
Figure 1: Number of smart contracts in Ethereum has increased found that 8, 833 contracts potentially have the documented
rapidly. bugs. These contracts currently have a total balance of
about 3, 068, 654 million Ethers, approximately equivalent
to 30 million USD at the time of writing. Moreover, Oyente
a smart contract’s execution by the network participants. can detect the infamous TheDAO bug, which caused a loss
For example, Ethereum (and Bitcoin) allow network partic- of 60 million US dollars to TheDAO’s investors in June
ipants (or miners) to decide which transactions to accept, 2016 [19]. We further discuss our results and our verified
how to order transactions, set the block timestamp and so attack with one of the most active contracts of Ethereum
on. Contracts which depend on any of these sources need to (affecting only our own accounts), in Section 6.
be aware of the subtle semantics of the underlying platform Although we use Ethereum’s smart contracts throughout
and explicitly guard against manipulation. this paper, Oyente and the security problems are largely
Unfortunately, the security of smart contracts has not platform agnostic. We believe Oyente can be extended to
received much attention, although several anecdotal inci- upcoming platforms such as CounterParty or Rootstock.
dents of smart contracts malfunctioning have recently been Contributions. This paper makes the following contribu-
reported, including contracts that do not execute as ex- tions.
pected [7, 12, 13] and/or that have locked away thousands of • We document several new classes of security bugs in Ethereum
dollars worth of virtual coins [7, 13]. In contrast to classical smart contracts.
distributed applications that can be patched when bugs are
• We formalize the semantics of Ethereum smart contracts
detected, smart contracts are irreversible and immutable.
and propose recomendations as solutions for the docu-
There is no way to patch a buggy smart contract, regardless
mented bugs.
of its popularity or how much money it has, without revers-
ing the blockchain (a formidable task). Therefore, reasoning • We provide Oyente, a symbolic execution tool which
about the correctness of smart contracts before deployment analyses Ethereum smart contracts to detect bugs.
is critical, as is designing a safe smart contract system. • We run Oyente on real Ethereum smart contracts and
In this paper, we document several new security flaws of confirmed the attacks in the real Ethereum network.
Ethereum smart contracts and give examples of real-world
instances for each problem. These security flaws make con-
tracts susceptible to abuse by several parties (including min- 2. BACKGROUND
ers and contracts’ users). We believe that these flaws arise We give a brief introduction to smart contracts and their
in practice because of a semantic gap between the assump- execution model. Our discussion is restricted to most pop-
tions contract writers make about the underlying execution ular smart contract platform called Ethereum, but the se-
semantics and the actual semantics of the smart contract curity problems discussed in this paper may be of wider
system. Specifically, we show how different parties can ex- application to other open distributed application platforms.
ploit contracts which have differing output states depending
on the order of transactions and input block timestamp. To 2.1 Consensus Protocol
our knowledge, these semantic gaps have not been previ- Decentralized cryptocurrencies secure and maintain a shared
ously identified. We also document other serious but known ledger of facts between a set of peer-to-peer network opera-
problems such as improperly handled aborts/exceptions and tors (or miners). Miners run a peer-to-peer consensus pro-
logical flaws. Previous work has discussed these conceptu- tocol called the Nakamoto consensus protocol. The shared
ally, often with simple self-constructed examples [14]. In our ledger is called a blockchain and is replicated by all miners.
work, we study their impact on tens of thousands of real-life The ledger is organized as a hash-chain of blocks ordered by
contracts, showing how these vulnerabilities can be used to time, wherein each block has a set of facts, as shown in Fig-
sabotage or steal coins from benign users. ure 2. In every epoch, each miner proposes their own block
More importantly, our work emphasizes the subtle and/or to update the blockchain. Miners can select a sequence of
missing abstractions in smart contract semantics that lead new transactions to be included in the proposed block. At
developers to a false sense of security. We propose refine- a high level, Nakamoto consensus works by probabilistically
ments to Ethereum’s protocol that do not require changes electing a leader among all the miners via a proof-of-work
to existing smart contracts. However, such solutions do re- puzzle [1]. The leader then broadcasts its proposed block
quire all clients in the network to upgrade, thus running the to all miners. If the proposed block obeys a certain pre-

255
 Time
Block i Block i+1 1 contract Puzzle {
2 address public owner ;
3 bool public locked ;
PrivBlock Nonce TimeStamp PrivBlock Nonce TimeStamp 4 uint public reward ;
5 bytes32 public diff ;
6 bytes public solution ;
ListOfTxs Blockchain state ListOfTxs Blockchain state 7
8 function Puzzle () // constructor {
9 owner = msg . sender ;
10 reward = msg . value ;
11 locked = false ;
12 diff = bytes32 (11111); // pre - defined difficulty
13 }
Balance Code Storage Update(PrevState, ListOfTxs) 14
15 function (){ // main code , runs at every invocation
Figure 2: The blockchain’s design in popular cryptocurrencies 16 if ( msg . sender == owner ){ // update reward
like Bitcoin and Ethereum. Each block consists of several trans- 17 if ( locked )
actions. 18 throw ;
19 owner . send ( reward );
20 reward = msg . value ;
21 }
22 else
defined validity constraints, such as those ensuring mitiga- 23 if ( msg . data . length > 0){ // submit a solution
tion of “double-spending” attacks, then all miners update 24 if ( locked ) throw ;
their ledger to include the new block. We exclude certain 25 if ( sha256 ( msg . data ) < diff ){
26 msg . sender . send ( reward ); // send reward
details about the consensus protocol, such as the use of the 27 solution = msg . data ;
longest-chain rule for resolving probabilistic discrepancies in 28 locked = true ;
leader election. Instead, we refer readers to the original Bit- 29 }}}}
coin or Ethereum paper for details [1, 2]. Figure 3: A contract that rewards users who solve a computa-
A blockchain state σ is a mapping from addresses to ac- tional puzzle.
counts; the state of an account at address γ is σ[γ]. While
Bitcoin only has normal accounts which hold some coins,
Ethereum additionally supports smart contract accounts which
have coins, executable code and persistent (private) stor- modify the blockchain state σ, adding a new contract ac-
age. Ethereum supports its own currency called Ether; users count in three following steps. First, a unique address for
can transfer coins to each other using normal transactions the new contract is prepared. Then the contract’s private
as in Bitcoin, and additionally can invoke contracts using storage is allocated and initialized by running the construc-
contract-invoking transactions. Conceptually, Ethereum can tor (i.e., Puzzle() function in Line 8). Finally, the executable
be viewed as a transaction-based state machine, where its EVM code portion that corresponds to the anonymous func-
state is updated after every transaction. A valid transition tion (Line 15 onwards) is associated with the contract.
T Any transaction invoking this contract will execute the
from σ to σ 0 , via transaction T is denoted as σ −→ σ 0 . anonymous function() (Line 15) by default. The informa-
tion of the sender, the value (amount of Ether sent to the
2.2 Smart Contracts in Ethereum contract) and the included data of the invocation transaction
A smart contract (or contract for short) is an “autonomous is stored in a default input variable called msg. For example,
agent” stored in the blockchain, encoded as part of a “cre- the contract owner updates the reward variable by invoking
ation” transaction that introduces a contract to the blockchain. a transaction To with some Ether (i.e., in msg.value). Be-
Once successfully created, a smart contract is identified by fore updating the reward variable to the new value (Line 20),
a contract address; each contract holds some amount of of the contract indeed sends back to the owner, an amount of
virtual coins (Ether), has its own private storage, and is Ether that is equal to the current reward value (Line 19).
associated with its predefined executable code. A contract The result of To is a new state of Puzzle which has a different
state consists of two main parts: a private storage and the reward value. Similarly, users can submit their solution in
amount of virtual coins (Ether) it holds (called balance). a different transaction payload (e.g., msg.data) to claim the
Contract code can manipulate variables like in traditional reward (Line 22–29). If the solution is correct, the contract
imperative programs. The code of an Ethereum contract is sends the reward to the submitter (Line 26).
in a low-level, stack-based bytecode language referred to as Gas system. By design, the smart contract is a mech-
Ethereum virtual machine (EVM) code. Users define con- anism to execute code distributively. To ensure fair com-
tracts using high-level programming languages, e.g., Solid- pensation for expended computation effort, Ethereum pays
ity [16] (a JavaScript-like language), which are then com- miners some fees proportional to the required computation.
piled into EVM code. To invoke a contract at address γ, Specifically, each instruction in the Ethereum bytecode has
users send a transaction to the contract address. A trans- a pre-specified amount of gas. When a user sends a transac-
action typically includes: payment (to the contract) for the tion to invoke a contract, she has to specify how much gas
execution (in Ether) and/ or input data for the invocation. she is willing to provide for the execution (called gasLimit)
An Example. Figure 3 is a simple contract, defined in as well as the price for each gas unit (called gasPrice). A
Solidity, which rewards anyone who solves a computational miner who includes the transaction in his proposed block
puzzle and submits the solution to the contract. The creator subsequently receives the transaction fee corresponding to
of the contract includes the compiled (EVM) code of Puzzle the amount of gas the execution actually burns multiplied
in a “contract creation” transaction. When such transaction by gasPrice. If some execution requires more gas than
is accepted to the blockchain, all miners will unanimously gasLimit, the execution is terminated with an exception,

256
the state σ is reverted to the initial state as if the execution 1 contract MarketPlace {
did not happen. In case of such aborts, the sender still has 2 uint public price ;
to pay all the gasLimit to the miner though, as a counter- 3 uint public stock ;
4 /.../
measure against resource-exhaustion attacks [6]. 5 function updatePrice ( uint _price ){
6 if ( msg . sender == owner )
7 price = _price ;
3. SECURITY BUGS IN CONTRACTS 8 }
We discuss several security bugs which allow malicious 9 function buy ( uint quant ) returns ( uint ){
10 if ( msg . value < quant * price || quant > stock )
miners or users to exploit and gain profit. 11 throw ;
12 stock -= quant ;
3.1 Transaction-Ordering Dependence 13 /.../
14 }}
As discussed in Section 2, a block includes a set of transac-
Figure 4: A contract that acts as a market place where users can
tions, hence the blockchain state is updated several times in
buy/ sell some tokens. Due to TOD, some order may or may not
each epoch. Let us consider a scenario where the blockchain go through.
is at state σ and the new block includes two transactions
(e.g., Ti , Tj ) invoking the same contract. In such a scenario,
users have uncertain knowledge of which state the contract 1 contract theRun {
2 uint private Last_Payout = 0;
is at when their individual invocation is executed. For exam- 3 uint256 salt = block . timestamp ;
ple, Ti is applied when the contract is at either state σ[α] or 4 function random returns ( uint256 result ){
Tj 5 uint256 y = salt * block . number /( salt %5);
state σ 0 [α] where σ −→ σ 0 , depending on the order between 6 uint256 seed = block . number /3 + ( salt %300)
Ti and Tj . Thus, there is a discrepancy between the state 7 + Last_Payout + y ;
of the contract that users may intend to invoke at, and the 8 // h = the blockhash of the seed - th last block
9 uint256 h = uint256 ( block . blockhash ( seed ));
actual state when their corresponding execution happens. 10 // random number between 1 and 100
Only the miner who mines the block can decide the order of 11 return uint256 ( h % 100) + 1;
these transactions, consequently the order of updates. As a 12 }}
result, the final state of a contract depends on how the miner Figure 5: A real contract which depends on block timestamp to
orders the transactions invoking it. We call such contracts send out money [22]. This code is simplified from the original
code to save space.
as transaction-ordering dependent (or TOD) contracts.

3.1.1 Attacks
It may be not obvious to the readers why having depen- onds. Thus, a malicious owner of the Puzzle contract can
dence on the transaction ordering is problematic for smart keep listening to the network to see if there is a transaction
contracts. The reasons are twofold. First, even a benign which submits a solution to his contract. If so, he sends his
invocation to the contract may yield an unexpected result transaction To to update the reward and make it as small as
to users if there are concurrent invocations. Second, a mali- zero. With a certain chance, both To and Tu are included in
cious user can exploit the TOD contracts to gain more prof- the new block and his To is placed (so executed) before the
its, even steal users’ money. We explain the two scenarios Tc . Thus the owner can enjoy a free solution for his puz-
below by using the Puzzle contract in Figure 3. zle. The owner can even bias the chance of his transaction
winning the race (i.e., to be executed first) by participating
Benign scenario. We consider two transactions To and
directly in the mining, setting higher gasPrice for his trans-
Tu sending to Puzzle at roughly the same time. To is from
action (i.e., to incentivize miners to include it in the next
the contract owner to update the reward and Tu is from
block) and/or colluding with other miners.
a user who submits a valid solution to claim the reward.
Since To and Tu are broadcast to the network at roughly
the same time, the next block will most likely include both
3.2 Timestamp Dependence
the transactions. The order of the two transactions decides The next security problem that a contract may have uses
how much reward the user receives for the solution. The the block timestamp as a triggering condition to execute
user expects to receive the reward that he observes when some critical operations, e.g., sending money. We call such
submitting his solution, but he may receive a different re- contracts as timestamp-dependent contracts.
ward if To is executed first. The problem is more significant A good example of a timestamp-dependent contract is the
if the contract serves as a decentralized exchange or market theRun contract in Figure 5, which uses a homegrown ran-
place [20, 21]. In these contracts, sellers frequently update dom number generator to decide who wins the jackpot [22].
the price, and users send their orders to buy some items Technically TheRun uses the hash of some previous block
(Figure 4). Depending on the transaction ordering, users’ as the random seed to select the winner (Line 9–10). The
buy requests may or may not go through. Even worse, buy- choice of block is determined based on the current block
ers may have to pay much higher than the observed price timestamp (Line 5–7).
when they issue the buy requests. Let us recall that when mining a block, a miner has to set
the timestamp for the block (Figure 2). Normally, the times-
Malicious scenario. The above scenario may just be an
tamp is set as the current time of the miner’s local system.
accident because the owner of Puzzle does not know when a
However, the miner can vary this value by roughly 900 sec-
solution is submitted. However, a malicious owner can ex-
onds, while still having other miners accept the block [23] 1 .
ploit transaction-ordering dependence to gain financial ad-
vantage. Note that there is a time gap between when trans- 1
The variation of block timestamp may now be less than 900
action Tu is broadcast and when it is included in a block. seconds according to the fact that Ethereum requires nodes
In Ethereum, the time to find a new block is around 12 sec- in the network to have roughly “same” local timestamps.

257
Specifically, on receiving a new block and after checking 1 contract K i n g O f T h e E t h e r T h r o n e {
other validity checks, miners check if the block timestamp is 2 struct Monarch {
greater than the timestamp of previous block and is within 3 // address of the king .
4 address ethAddr ;
900 seconds from the timestamp on their local system. Thus, 5 string name ;
the adversary can choose different block timestamps to ma- 6 // how much he pays to previous king
nipulate the outcome of timestamp-dependent contracts. 7 uint claimPrice ;
8 uint c o r o n a t i o n T i m e s t a m p ;
9 }
3.2.1 Attacks 10 Monarch public currentMonarch ;
A miner can set the block timestamp to be a specific 11 // claim the throne
12 function claimThrone ( string name ) {
value which influences the value of the timestamp-dependent 13 /.../
condition and favor the miner. For example in the theRun 14 if ( currentMonarch . ethAddr != wizardAddress )
contract, the hash of previous block and block number are 15 currentMonarch . ethAddr . send ( compensation );
16 /.../
known, other contract variables like last payout which con- 17 // assign the new king
tribute to the generation of the random seed are also known. 18 currentMonarch = Monarch (
Thus the miner can precompute and select the timestamp so 19 msg . sender , name ,
20 valuePaid , block . timestamp );
the function random produces an outcome that favors him. 21 }}
As a result, the adversary may completely bias the outcome Figure 6: A code snippet of a real contract which does not check
of the random seed to be any value, thus awarding the jack- the return value after calling other contracts [12].
pot to any player he pleases. Thus, theRun is vulnerable to
any adversary who can manipulate the block timestamp.
While theRun uses timestamp as a insecure deterministic
random seed, other contracts use block timestamp as global king. Thus, if for some reason, the compensation transaction
timestamp and perform some time-dependent computation. does not finish properly, the current king loses his throne
We show in Section 6 an example which uses timestamp for without any compensation. In fact, an instance of such a
this purpose and is vulnerable to manipulation. Unfortu- problem occurred and led to the termination of KoET [12].
nately, there are many other contracts which are timestamp- The reason reported in [12] is that the address Ak of the cur-
dependent. As we show in Section 6, among the first 19, 366 rent king is not a normal address, but a contract address.
contracts, 83 of them depend on the block timestamp to When sending a transaction (or call) to Ak , some code will
transfer Ether to different addresses. be executed, thus requiring more gas than a transaction to
a normal address. However, KoET does not know what Ak
3.3 Mishandled Exceptions executes internally beforehand to decide how much gas to
In Ethereum, there are several ways for a contract to call give in the send instruction. Hence Ak runs out of gas and
another, e.g., via send instruction or call a contract’s func- throws an exception. As a result, the state (and balance)
tion directly (e.g.,aContract.someFunction()). If there is an of Ak remains unchanged, the compensation is returned to
exception raised (e.g., not enough gas, exceeding call stack KoET and the current king loses his throne without any
limit) in the callee contract, the callee contract terminates, compensation.
reverts its state and returns false. However, depending on The above problem often arises when a contract sends
how the call is made, the exception in the callee contract money to a dynamic address, since the sender does not know
may or may not get propagated to the caller. For example, how much gas to allocate for the transaction. The contract
if the call is made via the send instruction, the caller con- should always check if the transaction succeeds before exe-
tract should explicitly check the return value to verify if the cuting subsequent logic. The callee contract may throw an
call has been executed properly. This inconsistent exception exception of any type (e.g., division by zero, array index out
propagation policy leads to many cases where exceptions are of bound and so on).
not handled properly. As we later show in Section 6, 27.9% In this scenario, the recipient (or callee) seems at fault,
of the contracts do not check the return values after call- causing the send to fail. However, as we show next, a mali-
ing other contracts via send. We discuss the threats of not cious user who invokes the caller contract can cause the send
validating return value of a contract call via our example in to fail deliberately, regardless of what the callee does.
Figure 6, which is a code snippet of a real contract [12]. Deliberately exceeding the call-stack’s depth limit.
The Ethereum Virtual Machine implementation limits the
3.3.1 Attacks call-stack’s depth to 1024 frames. The call-stack’s depth
The KingOfTheEtherThrone (KoET for short) contract in increases by one if a contract calls another via the send or
Figure 6 allows users to claim as “king of Ether” by paying call instruction. This opens an attack vector to deliberately
some amount of Ether that the current king requires. A king cause the send instruction in Line 15 of KoET contract to
gets profit (i.e., compensation) from the difference between fail. Specifically, an attacker can prepare a contract to call
the price he paid to the king before him and the price other itself 1023 times before sending a transaction to KoET to
pays to be his successor. When a user claims the throne, the claim the throne from the current king. Thus, the attacker
contract sends the compensation to the ceded king (Line 15), ensures that the call-stack’s depth of KoET reaches 1024,
and assigns the user as the new king (Line 18—20). causing the send instruction in Line 15 to fail. As the result,
The KoET contract does not check the result of the com- the current king will not receive any payment. This call-
pensation transaction in Line 15 before assigning the new stack problem was identified in a previous report [24], but
remains unfixed in the current Ethereum protocol.
However, we could not find any updated document from
Ethereum regarding the new possible variation, thus keeping Exploiting call stack limit to gain benefit. In the previ-
900 seconds. ous attack to KoET, the attacker does not receive any direct

258
 1 contract SendBalance { Section 3. Despite being lightweight, our formalism rigor-
2 mapping ( address = > uint ) userBalances ; ously captures interesting features of Ethereum, exposing
3 bool withdrawn = false ; the subtleties in its semantics, which further enables us to
4 function getBalance ( address u ) constant returns ( uint ){
5 return userBalances [ u ]; state our proposed solutions precisely.
6 } We use the following notation: ← to denote assignment,
7 function addToBalance () { • to denote an arbitrary element (when the specific value
8 userBalances [ msg . sender ] += msg . value ;
9 } is important), ⇓ to denote big-step evaluation, and ; to
10 function with drawBalance (){ denote small-step evaluation. Finally, a[i 7→ v] returns a
11 if (!( msg . sender . call . value ( new array identical to a, but on position i contains the value
12 userBalances [ msg . sender ])())) { throw ; }
13 userBalances [ msg . sender ] = 0; v; this notation of array update also applies to nested arrays.
14 }}
Figure 7: An example of the reentrancy bug. The contract im- 4.1 Operational Semantics of Ethereum
plements a simple bank account. Recall (from Section 2) that a canonical state of Ethereum,
denoted by σ, is a mapping between addresses and account
states. We write a valid transition from σ to σ 0 via transac-
T
benefit besides causing other users to lose their entitlement. tion T as σ −→ σ 0 .
However, in many other examples, the attacker can exploit Formation and Validation of a Block. To model the
to directly benefit as well. In Ethereum, many contracts formation of the blockchain and the execution of blocks, we
implement verifiable Ponzi (or pyramid) schemes [22,25,26]. define a global Ethereum state as a pair hBC, σi, where BC
These contracts pay investors interest for their investments is the current block chain and σ is as before. Γ denotes the
from the subsequent investments by others. An attacker can stream of incoming new transactions. For simplicity, we do
invest his money, make payments to previous investors fail not model miner rewards.
so he can receive his interest early. We discuss one of such
contracts in Section 6. Specifically, we show that 5, 411 con-
TXs ← Some transaction sequence (T1 . . . Tn ) from Γ
tracts (27.9%) are vulnerable to attacks that deliberately ex-
B ← hblockid ; timestamp ; TXs ; . . . i
ceed the call-depth limit. We also conduct the attack in one
of the most popular contracts in Ethereum (with no harm proof-of-work(B, BC)
T
i
to others, but our own accounts) to confirm our finding. ∀ i, 1 ≤ i ≤ n : σi−1 −→ σi
Propose
hBC, σ0 i ⇓ hB · BC, σn i
3.4 Reentrancy Vulnerability Remove T1 . . . Tn from Γ and broadcast B
Reentrancy is a well-known vulnerability with a recent
TheDao hack [19], where the attacker exploited the reen-
Receive B ≡ hblockid ; timestamp ; TXs ; . . . i
trancy vulnerability to steal over 3, 600, 000 Ether, or 60
TXs ≡ (T1 . . . Tn )
million US Dollars at the time the attack happened. For Ti
the completeness of this paper, we discuss the vulnerability ∀ i, 1 ≤ i ≤ n : σi−1 −→ σi
Accept
here as we later on describe how one can implement reen- hBC, σ0 i ⇓ hB · BC, σn i
trancy’s detection in our tool Oyente in Section 5.
Remove T1 . . . Tn from Γ and broadcast B
In Ethereum, when a contract calls another, the current
execution waits for the call to finish. This can lead to an Figure 8: Proposing and Accepting a Block
issue when the recipient of the call makes use of the inter-
mediate state the caller is in. This may not be immediately The actions of the miners to form and validate blocks
obvious when writing the contract if possible malicious be- are given in Figure 8. Only one “elected leader” executes
havior on the side of the callee is not considered. successfully the Propose rule at a time. Other miners use
Attack example. We can see an example of this attack the Accept rule to “repeat” the transitions σi−1 −→
Ti
σi after
in sendBalance (Figure 7). The contract being called by the leader broadcasts block B.
sendBalance can simply call it again, since the balance for
this contract has not yet been set to zero. In Figure 7, Security Issues: As discussed earlier, the issue of timestamp-
Line 15 sends the current balance of the withdrawer — as dependence arises because the elected leader has some slack
indicated by the internal variable userBalances — to the in setting the timestamp, yet other miners still accept the
contract address wishing to withdraw its balance. How- block. On the other hand, the issue of transaction-ordering-
ever, the variable userBalances is only zeroed after the call is dependence exists because of some inevitable order among
made, which means that the persistent storage of the con- Ti ; yet we have shown that when dealing with Ether (or
tract which records users’ balances has not yet been altered. money), this might lead to undesirable outcomes.
The callee contract of the call in Line 15, using its default Transaction Execution. A transaction can activate the
function, can call withdrawBalance until the contract is emp- code execution of a contract. In Ethereum, the execution
tied of Ether — or it depletes available gas — whichever can access to three types of space in which to store data:
comes first. (1) an operand LIFO stack s; (2) an auxiliary memory l,
an infinitely expandable array; and (3) the contract’s long-
term storage str, which is part of σ[id] for a given contract
4. TOWARDS A BETTER DESIGN address id. Unlike stack and auxiliary memory, which reset
We formalize a “lightweight” semantics for Ethereum in after computation ends, storage persists as part of σ.
Section 4.1, and then build on this formalism in Section 4.2 We define a virtual machine’s execution state µ as a config-
to recommend solutions to the security issues identified in uration hA, σi, where A is a call stack (of activation records)

259
and σ is as before. The activation record stack is defined as: equal to zero”. It pops two elements z and λ from the top of
∆
the operand stack; if z is nonzero then the program counter
A = Anormal | heiexc · Anormal is set to λ, otherwise it is the program counter is incre-
∆
Anormal = hM, pc, l, si · Anormal |  mented. The load and store instructions respectively reads
from and writes to memory in the natural way. However,
where  denotes an empty call stack; heiexc denotes that an here we have two types of load and store, dealing with two
exception has been thrown; and each part of an activation types of memory mentioned above. While mload and mstore
record hM, pc, l, si has the following meaning: deal with the auxiliary memory l, sload and sstore respec-
M : the contract code array tively assesses and updates the contract storage str, i.e., the
pc : the address of the next instruction to be executed state of the contract.
l : an auxiliary memory (e.g. for inputs , outputs) Let us now discuss more interesting instructions inspired
s : an operand stack. from Ethereum. The key instructions are call and return,
Though a transaction in Ethereum is a complex structure whose operational semantics are provided in Table 12 . Each
and specifies a number of fields, we abstract it to a triple row describes the conditions under which an execution can
hid, v, li where id is the identifier of the to-be-invoked con- move from configuration µ to configuration µ0 , i.e. µ ; µ0 .
tract, v is the value to be deposited to the contract, and l The first column indicates the instruction form captured by
is an data array capturing the values of input parameters. the rule. If the instruction about to be executed matches
Thus a transaction execution can be modeled with the rules that form and all the (side) conditions in the second column
in Figure 9: the first rule describes an execution that ter- are satisfied, then a step may be made from a configuration
minates successfully (or “normal halting”) while the second matching the pattern in the third column to a configuration
rule describes one that terminates with an exception. matching the pattern in the last column.
Note that the execution of a transaction is intended to A call instruction is roughly analogous to a remote pro-
follow the “transactional semantics” of which two important cedure call3 . The arguments placed on the operand stack,
properties are: (1) Atomicity, requiring that each transac- are the destination γ, amount of Ether to transfer z, and two
tion be “all or nothing”. In other words, if one part of the values st and sz (for “start address” and “size”) to specify a
transaction fails, then the entire transaction fails and the slice of memory which contains additional function-specific
state is left unchanged; and (2) Consistency, ensuring that parameters. The next two values in the operand stack simi-
any transaction will bring the system from one valid state to larly specify a place for the return value(s); they are exposed
another. We will show, later in this section, how these prop- (in the rules) when the call is returned, or an exception has
erties might be violated, when we discuss the operational occurred. Unlike the operand stack, which has no fixed max-
semantics of EVM instructions. imum size, the call stack has a maximum size of 1, 024. If
the call stack is already full then the remote call will cause
T ≡ hid, v, li M ← Lookup(σ, id) an exception (second rule for call). When the remote call
σ 0 ← σ[id][bal 7→ (σ[id][bal] + v)] returns, a special flag is placed onto the operand stack, with
hhM, 0, l, i · , σ 0 i ;∗ h, σ 00 i 1 indicating a successful call (second rule for return) and 0
TX-success indicating an unspecified exception (rule EXC).
T
σ −→ σ 00 There are two important points to note. First, an excep-
tion at a callee is not limited to (call) stack overflow. It could
T ≡ hid, v, li M ← Lookup(σ, id) be due to various reasons such as gas exhaustion, division by
σ 0 ← σ[id][bal 7→ (σ[id][bal] + v)] zero, etc. Second, exceptions are not propagated automat-
hhM, 0, l, i · , σ 0 i ;∗ hheiexc · , •i ically. Contract writers who wish to do so must explicitly
TX-exception
T check for the 0 and then raise a new exception, typically
σ −→ σ
by jumping to an invalid label. For certain high-level com-
Figure 9: Rules for Transaction Execution. Lookup(σ,id) finds mands in Solidity, a code snippet to perform these steps is
the associated code of contract address id in state σ; σ[id][bal]
inserted by the compiler.
refers to the balance of the contract at address id in state σ.
Security Issues: Recall the security issues discussed in Sec-
tion 3.3, in particular when exceptions are mishandled. The
Execution of EVM Instructions. We have distilled EVM root cause of the problem is in the inconsistency of how ex-
into a language EtherLite, which is a stack machine aug- ceptions influence the final state, depending whether a con-
mented with a memory and some Ethereum-like features. tract method is invoked as a transaction, or via the call
The instructions ins ∈ instruction of EtherLite are: instruction. In the former case, rule TX-exception in Fig-
∆ ure 9, the execution is aborted ; while in the latter case, row
ins = push v | pop | op | bne | exc Table 1, a flag 0 is pushed into the operand stack of the
mload | mstore | sload | sstore | caller. The way that an exception occurs at a callee, and
call | return | suicide | create | getstate is converted into a flag 0 (and the execution continues nor-
The push instruction takes an argument v ∈ value which is mally) indeed breaks the atomicity property. In other words,
either a numeric constant z, code label λ, memory address Ethereum transactions do not have atomicity in their seman-
α, or contract/recipient address γ and adds it to the top of tics. This can lead to serious consequences, especially given
the “operand stack”. The pop instruction removes (forgets) 2
For completeness, operational semantics of other instruc-
the top element of the operand stack. The op instruction, tions are provided in the Appendix.
representing all of the arithmetic and logical etc. operations, 3
Ethereum has several additional variants of call, includ-
pops its arguments, performs the operation, and pushes the ing CALLCODE and DELEGATECALL which we do not model in
result. Conditional branch bne is a standard “branch if not EtherLite.

260
 Table 1: Operational Semantics of call and return. EXC stands for “Exception”.

M [pc] Conditions µ µ0
id ← address of the executing contract
a0 ← hM, pc, l, si
call M 0 ← Lookup(σ, γ) hhM, pc, l, γ · z · st · sz · si · A, σi hhM 0 , 0, l0 , i · a0 · A, σ 00 i
σ 0 ← σ[id][bal 7→ σ[id][bal] − z]
σ 00 ← σ 0 [γ][bal 7→ σ[id][bal] + z]
id ← address of the executing contract
call hhM, pc, l, • · v · • · • · • · • · si · A, σi hhM, pc + 1, l, 0 · si · A, σi
σ[id][bal] < v or |A| = 1023
return hhM, pc, •, •i · , σi h, σi
a0 ≡ hM 0 , pc0 , l00 , st0 · sz 0 · s0 i
return n ← min(sz 0 , sz) hhM, pc, l, st · sz · si · a0 · A, σi hhM 0 , pc0 + 1, ln0 , 1 · s0 i · A, σi
0
0 ≤ i < n : li+1 ← li0 [st0 + i 7→ l[st + i]]
EXC exceptional halting of callee hheiexc · hM, pc, l, st · sz · si · A, σi hhM, pc + 1, l, 0 · si · A, σi

that money transfers in Ethereum are mostly done using the 4.2 Recommendations for Better Semantics
call instruction. We propose improvements to the operational semantics
There are three remaining instructions: suicide, cre- of Ethereum to fix the security problems discussed in Sec-
ate, and getstate. The suicide instruction transfers all of tion 3. To deploy these proposals, all clients in the Ethereum
the remaining Ether to recipient γ and then terminates the network must upgrade.
contract; although somewhat similar to call in that Ether
changes hands, it does not use the call stack. The create 4.2.1 Guarded Transactions (for TOD)
instruction creates a new contract account, taking three ar- Recall that a TOD contract is vulnerable because users are
guments from the operand stack. They are the amount of uncertain about which state the contract will be in when
Ether to be put in the new contract, and two values to spec- their transactions is executed. This seems inevitable be-
ify a slice of memory which contains the bytecode for the cause miners can set arbitrary order between transactions
new contract. It proceeds in three steps: (rule Propose). To eliminate the TOD problem, we need
1. Creating a new address and allocating storage for the to guarantee that an invocation of a contract code either
new contract. The specified amount of Ether is also returns the expected output or fails, even given the inherent
deposited into the contract. non-deterministic order between selected transactions.

2. Initializing the contract’s storage.

T ≡ hg, •, •, •i σ 6` g
3. Depositing the associated code body into the contract. TX-stale
T
σ −→ σ
If the contract creation is successful, the address of new
contract is pushed onto the operand stack; otherwise, a flag T ≡ hg, id, v, li M ← Lookup(σ, id)
value of 0 is pushed. The three above-mentioned steps rely σ`g σ 0 ← σ[id][bal 7→ (σ[id][bal] + v)]
on certain helper procedures, which we will not attempt to hhM, 0, l, i · , σ 0 i ;∗ h, σ 00 i
capture with our formalism. Note that: (1) while the initial- TX-success
T
ization code is executing, the newly created address exists σ −→ σ 00
but with no intrinsic body code; and (2) if the initialization
T ≡ hg, id, v, li M ← Lookup(σ, id)
ends up with an exception then the state is left with a “zom-
σ`g σ 0 ← σ[id][bal 7→ (σ[id][bal] + v)]
bie” account, and any remaining balance will be locked into
hhM, 0, l, i · , σ 0 i ;∗ hheiexc · , •i
the account forever. In other words, an unsuccessful con- TX-exception
T
tract creation might lead to an invalid contract residing in σ −→ σ
the system, breaking the consistency property of the “trans- Figure 10: New Rules for Transaction Execution.
actional semantics”. This issue might not directly lead to
some security attacks, it is clearly undesirable in the cur-
rent design of Ethereum. Guard Condition. Our new rules for transaction execu-
Lastly, getstate is an abstract instruction of which the tion are given in Figure 10. A transaction T now addition-
concrete instance related to the security problem in 3.2 is ally specifies a guard condition g; the current state σ needs
to get the current block timestamp. A getstate instruction to satisfy g for the execution of T to go through. If g is not
typically pushes certain “special” value onto the stack: in satisfied, the transaction is simply dropped by the new rule
particular, the current timestamp, block id, remaining gas, TX-stale. For transactions which do not provide g, we sim-
current balance, and this contract’s own address. Note that ply consider g ≡ true. This solution guarantees that either
some of these values should be thought of as constants (e.g. the sender gets the expected output or the transaction fails.
current timestamp, block id), while others are updated in The solution is also backward-compatible because we do not
tandem with the execution of a transaction (e.g. remaining require changes in existing contract code: old transactions
gas, current balance). can simply take the default guard condition true.
To illustrate, let us revisit the Puzzle contract in Sec-

261
tion 3.1. A user who submits a transaction Tu to claim
the reward should specify the condition g ≡ (reward == R), ByteCode CFG Builder Visualizer
where R is the current reward stored in the contract. If the
owner’s transaction is executed first, g is invalidated and
the user’s transaction Tu will abort, meaning the owner will Ethereum EXPLORER
CORE VALIDATOR
State ANALYSIS
not get the solution4 . Note that Puzzle is only one example
of a more serious class of contracts serving as decentralized
exchanges or market places (see Section 3.1). With our so- Z3 Bit-Vector Solver
lution, buyers can easily avoid paying a price much higher
than what they observe when issuing the buy orders. Figure 11: Overview Architecture of Oyente. Main components
Note that “guarded transactions” resemble the “compare- are within the dotted area. Shaded boxes are publicly available.
and-swap” (CAS) instruction supported by most modern
processors. CAS is a key standard multithreaded synchro-
nization primitive, and “guarded transactions” equips Ether- does not help when the contract owner/writer is malicious
eum with equivalent power. and deliberately plants a bug in the contract.

4.2.2 Deterministic Timestamp 5. THE Oyente TOOL

Allowing contracts to access to the block timestamp is Our solutions proposed in the previous Section do require
essentially a redundant feature that renders contracts vul- all clients in the network to up-grade, thus running the risk
nerable to manipulation by adversaries. Typically, block of not seeing real deployment. As a pre-deployment mitiga-
timestamp is used for two purposes: serving as a deter- tion, we provide a tool called Oyente to help: (1) develop-
ministic random seed (e.g., in theRun contract) and as a ers to write better contracts; and (2) users to avoid invoking
global timestamp in a distributed network (in [25, 26, 28]). problematic contracts. Importantly, other analyses can also
Using block timestamp as a random seed is not wise since be implemented as independent plugins, without interfering
the entropy is low and the timestamp is easy to manipu- with our existing features. E.g., a straightforward exten-
late. There are ways to obtain better random seeds on the sion of Oyente is to compute more precise estimation of
blockchain [29, 30]. worst-case gas consumption for contracts.
Rather than using the easily-manipulable timestamp, con- Our analysis tool is based upon symbolic execution [31].
tracts should use the block index—a new block is created ap- Symbolic execution 5 represents the values of program vari-
proximately every 12 seconds in Ethereum—to model global ables as symbolic expressions of the input symbolic values.
time. The block index always increments (by one), removing Each symbolic path has a path condition which is a formula
any flexibility for an attacker to bias the output of contract over the symbolic inputs built by accumulating constraints
executions that access the time. which those inputs must satisfy in order for execution to fol-
A practical fix is to translate existing notions of times- low that path. A path is infeasible if its path condition is
tamp into block numbers. The change can be implemented unsatisfiable. Otherwise, the path is feasible.
by returning the block id for the instruction TIMESTAMP and We choose symbolic execution because it can statically
translating the associated expressions. For example, the reason about a program path-by-path. On one hand, this is
condition timestamp - lastTime > 24 hours can be rewrit- superior to dynamic testing, which reasons about a program
ten as blockNumber - lastBlock > 7,200. This implementa- input-by-input. For Ethereum, dynamic testing would even
tion requires changes to only the getstate instruction from require much more effort to simulate the execution envi-
Section 4.1. ronment. As an example, to detect the transaction-ordering
dependence, we must compare the outcomes of the interleav-
4.2.3 Better Exception Handling ing of different execution paths. It is difficult to approach
A straightforward solution is to check the return value this with dynamic testing, given the non-determinism and
whenever a contract calls another. Currently, the Solid- complexity of the blockchain behaviors.
ity compiler inserts a code snippet to perform exception On the other hand, by reasoning about one path at a
forwarding, except when the call is made via send or call, time, symbolic execution can achieve better precision (or
which are considered low-level instructions (from Solidity less false positives) compared to traditional approaches us-
point of view). This half-way solution still leaves the “atom- ing static taint analysis or general data flow analysis. In
icity property” broken. those approaches, abstract program states are often merged,
A better solution is to automatically propagate the excep- admitting states that never happen in a real execution, and
tion at the level of EVM from callee to caller; this can be eventually lead to high false positives.
easily implemented but requires all clients to upgrade. We
can additionally provide a mechanism for proper exception 5.1 Design Overview
handling, e.g., by having explicit throw and catch EVM in- Figure 11 depicts the architecture overview of Oyente.
structions. If an exception is (implicitly or explicitly) thrown It takes two inputs including bytecode of a contract to be
in the callee and not properly handled, the state of the caller analyzed and the current Ethereum global state. It answers
can be reverted. This approach and has been used in many whether the contract has any security problems (e.g., TOD,
popular programming languages including C++, Java and timestamp-dependence, mishandled exceptions), outputting
Python. Note that adding throw and catch instructions “problematic” symbolic paths to the users. One by-product
4 of our tool is the Control Flow Graph (CFG) of the contract
Owners can read the solution from the transaction data if
5
it is in plain-text, but solutions to this are well-studied [6, Symbolic execution can also be viewed as abstract inter-
14, 27]. pretation [32].

262
bytecode. We plan that in the future Oyente will be able paths which exhibit distinct flows of Ether. Thus, we detect
to work as an interactive debugger, thus we feed the CFG if a contract is TOD if it sends out Ether differently when
and the problematic paths into a Graph Visualizer. the order of transactions changes. Similarly, we check if a
The bytecode is publicly available on the blockchain and contract is timestamp-dependent if the condition to send in-
Oyente interprets EVM instruction set to faithfully maps cludes the block timestamp. We describe how we implement
instructions to constraints, i.e., bit-level accuracy. The Ether- our analyses as below.
eum global state provides the initialized (or current) values • TOD detection. Explorer returns a set of traces and the
of contract variables, thus enabling more precise analysis. corresponding Ether flow for each trace. Our analysis thus
All other variables including value, data of message call are checks if two different traces have different Ether flows. If
treated as input symbolic values. a contract has such pairs of traces, Oyente reports it as
Oyente follows a modular design. It consists of four main a TOD contract.
components, namely CFGBuilder, Explorer, CoreAnalysis and
Validator. CFGBuilder constructs a Control Flow Graph of • Timestamp dependence detection. We use a special sym-
the contract, where nodes are basic execution blocks, and bolic variable to represent the block timestamp. Note that
edges represent execution jumps between the blocks. Ex- the block timestamp stays constant during the execution.
plorer is our main module which symbolically executes the Thus, given a path condition of a trace, we check if this
contract. The output of Explorer is then fed to the CoreAnal- symbolic variable is included. A contract is flagged as
ysis where we implement our logic to target the vulnerabili- timestamp-dependent if any of its traces depends on this
ties identified in Section 3. Finally, Validator filters out some symbolic variable.
false positives before reporting to the users. • Mishandled exceptions. Detecting a mishandled exception
is straightforward. Recall that if a callee yields an excep-
5.2 Implementation tion, it pushes 0 to the caller’s operand stack. Thus we
We implement Oyente in Python with roughly 4, 000 only need to check if the contract executes the ISZERO
lines of code. Currently, we employ Z3 [33] as our solver to instruction (which checks if the top value of the stack is
decide satisfiability. Oyente faithfully simulates Ethereum 0) after every call. If it does not, any exception occurred
Virtual Machine (EVM) code which has 64 distinct instruc- in the callee is ignored. Thus, we flags such contract as a
tions in its language. Oyente is able to detect all the three contract that mishandles exceptions.
security problems discussed in Section 3. We describe each • Reentrancy Detection. We make use of path conditions in
component below. order to check for reentrancy vulnerability. At each CALL
CFG Builder. CFGBuilder builds a skeletal control flow that is encountered, we obtain the path condition for the
graph which contains all the basic blocks as nodes, and some execution before the CALL is executed. We then check if
edges representing jumps of which the targets can be de- such condition with updated variables (e.g., storage val-
termined by locally investigating the corresponding source ues) still holds (i.e., if the call can be executed again). If
nodes. However, some edges cannot be determined stat- so, we consider this a vulnerability, since it is possible for
ically at this phase, thus they are constructed on the fly the callee to re-execute the call before finishing it.
during symbolic execution in the later phase.
Validation. The last component is Validator which at-
Explorer. Our Explorer starts with the entry node of the tempts to remove false positives. For instance, given a con-
skeletal CFG. At any one time, Explorer may be executing a tract flagged as TOD by CoreAnalysis and its two traces t1
number of symbolic states. The core of Explorer is an inter- and t2 exhibiting different Ether flows, Validator queries Z3
preter loop which gets a state to run and then symbolically to check if both ordering (t1 , t2 ) and (t2 , t1 ) are feasible. If
executes a single instruction in the context of that state. no such t1 and t2 exist, the case is considered as a false
This loop continues until there are no states remaining, or positive. However, because we have not fully simulated the
a user-defined timeout is reached. execution environment of Ethereum, Validator is far from
A conditional jump (JUMPI) takes a boolean expression being complete. For the results presented in Section 6, we
(branch condition) and alters the program counter of the resort to best-effort manual analysis to confirm the security
state based on whether the condition is true or false. Ex- bugs. In other words, the current main usage of Oyente
plorer queries Z3 to determine if the branch condition is ei- is to flag potentially vulnerable contracts; full-fledged false
ther provably true or provably false along the current path; positive detection is left for future work.
if so, the program counter is updated to the appropriate tar-
get address. Otherwise, both branches are possible: we then
explore both paths in Depth First Search manner, updating 6. EVALUATION
the program counter and path condition for each path ap- We measure the efficacy of Oyente via quantitative and
propriately. More edges might be added to the skeletal CFG. qualitative analyses. We run Oyente on all contracts in the
At the end of the exploration phase, we produce a set of first 1, 459, 999 blocks of Ethereum. Our goals are three-
symbolic traces. Each trace is associated with a path con- fold. First, we aim to measure the prevalence of the security
straint and auxiliary data that the analyses in later phase bugs discussed in Section 3 in the real Ethereum contracts.
require. The employment of a constraint solver, Z3 in par- Second, we highlight that our design and implementation
ticular, helps us eliminate provably infeasible traces from choices are driven by the characteristics of real-life smart
consideration. contracts, and that Oyente is robust enough to handle
Core Analysis. CoreAnalysis contains sub-components to them. Lastly, we present several case studies demonstrat-
detect contracts which are TOD, timestamp-dependent or ing misunderstandings that many contract developers have
mishandled exceptions. Currently, the Explorer collects only about the subtle semantics of Ethereum.

263
 14000 50
5,411
No. of contracts No. of instructions
45
No. of unique contracts 12000 No. of distinct instructions
40

10000 35
4,000

Distinct Instructions
Total instructions
30
3,056 8000
25
6000
20
2,000
1,385 4000 15

10
340186 2000
135 5
83 52
0 0 0
0 2000 4000 6000 8000 10000 12000 14000 16000 18000 20000

Exception TOD Reentrancy Timestamp

Contracts (numbered from 1 to 19, 366)
Figure 12: Number of buggy contracts per each security problem
reported by Oyente.
Figure 13: Number of instructions in each contract

6.1 Benchmarks and Tool Robustness

We collected 19, 366 smart contracts from the blockchain tracts which have at least one security issue discussed in
as of May 5, 2016. These contracts currently hold a total Section 3. Out of these, 1, 682 are distinct (by direct com-
balance of 3, 068, 654 Ether, or 30 Million US dollars at the parison of the bytecode). Of these, we were able to collect
time of writing. The balance in contracts vary significantly: source code for only 175 contracts to confirm the tool’s cor-
most of contracts do not hold any Ether (e.g., balance is rectness; we manually check for false positives. Among all
zero), 10% of them have at least 1 Ether, while the highest contracts with source, Oyente has a low false positive rate
balance (2, 401, 557 Ether) accounts for 38.9% of the total of 6.4%, i.e., only 10 cases out of 175.
balance in all contracts. On an average, a contract has 318.5 Mishandled exceptions. 5, 411 contracts have mishan-
Ether, or equivalently 4523 US dollars. This suggests that dled exceptions flagged by Oyente, which account for 27.9%
attackers are well-incentivized to target and exploit flaws in of the contracts in our benchmark. Out of these 5, 411 con-
smart contracts to gain profit. tracts, 1, 385 are found to be distinct and 116 contracts have
Ethereum contracts vary from being simple to fairly com- source code available. By manual analysis, we verify that
plex. Figure 13 shows that the number of instructions in a all these 116 contracts are true positives. In order to con-
contract ranges from 18 to 23, 609, with an average of 2, 505 firm, we identify if any external calls (SEND, CALL instruc-
and a median of 838. The number of distinct instructions tions) are present and not followed by any checks for failures.
used in a single contract is shown in Figure 13. It shows These failure checks are implemented by verifying if the re-
that to handle these real-world contracts, Oyente needs turn value is non-zero.
to correctly handle the logic of 63 instructions. We choose The prevalence of this problem is explained by the follow-
to build Oyente on EVM bytecode rather than the source ing observation. In the first 1, 459, 999 blocks on the public
code (e.g., Solidity [16]) because only a small number con- blockchain, 180, 394 cross-contract calls were processed. For
tracts have source code publicly available on public repos- each contract invocation, there may be additional calls to
itories [34, 35]. Oyente finds a total number of 366, 213 other contracts, thus increasing the call-stack depth. These
feasible execution paths which took a total analysis time of can be due to function or library calls, external account
roughly 3, 000 hours on Amazon EC2. transactions, or nested recursive contract calls. We plot the
call-stack depths of these contract invocations in Figure 14,
6.2 Quantitative analysis which shows that most of them involve some level of nesting
Experimental setup. We run Oyente on 19, 366 con- (e.g., invoking other contracts). Further, all contract invo-
tracts in our benchmark. All experiments are conducted on cations do not exceed the call-stack depth of 50 in benign
4 Amazon EC2 m4.10xlarge instances, each has 40 Ama- runs, which is far below the call-stack depth’s limit of 1, 024.
zon vCPU with 160 GB of memory and runs 64-bit Ubuntu This explains why exceptions are commonly unexpected and
14.04. We use Z3 v4.4.1 as our constraint solver [33]. We unhandled in benign invocations.
set a timeout for our symbolic execution (e.g.,Explorer com- Transaction-ordering dependence. The TOD contracts
ponent) of 30 mins per contract. The timeout for each Z3 are less common with 3, 056 contracts, or 15.7% of the con-
request is set to 1 second. tracts in our benchmarks. Of these contracts, there are 135
Performance. On average, Oyente takes 350 seconds to distinct contracts and 32 have source code available. We
analyze a contract. 267 contracts require more than 30 min- manually verify that 9 of them are false positives and 23
utes to analyze. The number of paths explored by Oyente are true positives. In order to confirm, we look for different
ranges from 1 to 4613 with an average of 19 per contract flows of Ether wherein the outcome depends on the order of
and a median of 6. We observe that the running time de- the input transactions.
pends near linearly on the number of explored paths, i.e., Several true positive cases, where this dependence is ex-
the complexity of contracts. ploitable, are discussed later. As an example of a false pos-
itive, Figure 15 shows a case where there are two separate
6.2.1 Results flows of Ether, but the order of their execution does not
Figure 12 reports our results. Oyente flags 8, 833 con- change the outcome of the contract. The first flow (send

264
 ·104
1 function enter (){
2 uint amount = msg . value ;
6 3 if (( amount < contribution )...) {
4 msg . sender . send ( msg . value );
Number of Invocations
5 return ;
6 }
7 addParticipant ( msg . sender , inviter );
4
8 address next = inviter ;
9 uint rest = amount ;
10 uint level = 1;
11 while ( ( next != top ) && ( level < 7) ){
2 12 uint toSend = rest /2;
13 next . send ( toSend );
14 /.../
15 }
0 16 next . send ( rest );
17 Tree [ next ]. totalPayout += rest ;
0 10 20 30 40 50 18 }
Call-stack depth Figure 15: A false positive TOD contract flagged by Oyente.
Figure 14: Call-stack depth statistics in 180, 394 contract This contract implements a typical ponzi scheme.
invocations in Ethereum network

• After 12 hours without no new investment, the last in-

in Line 4) returns Ether to the sender if some requirement vestor and the contract owner shares the jackpot.
is not met, while the latter (Line 7–17) pays out to previ- The code to handle the last step is in Figure 17. Line 7
ous participants. Oyente recognized the two flows of Ether and 9 use send instructions to send Ether, which may not
and flagged the contract as potentially buggy. However, the execute correctly as discussed in Section 3.3. The contract
order in which these flows are executed by incoming trans- does not check if the operations were successful, leaving it
actions does not affect the intended payouts and recipients vulnerable to attack.
therein. The tool could involve more time-consuming anal-
yses to resolve such cases in the future. The final state of Stealing Ether from investors. Let us consider the code
the contract remains the same. snippet from Figure 17 which has a subtle bug. Line 11
seems harmless in that it pays out the owners after all cred-
Timestamp dependence. Oyente reports 83 timestamp- itors have been paid, with all remaining amount. However,
dependent contracts in our benchmark, out of which 52 are if the owners were to call the contract with a carefully con-
distinct. Only 7 of these have source code available, which structed call-stack size of 1023, none of the send instructions
we manually verified for false positives. To confirm, we check would succeed, resulting in no Ether going out. A second
if timestamp is included in the path condition of a flow of call to the contract would result in the owners receiving the
Ether, such that manipulation of the block timestamp would entirety of the contract’s balance and forcing previous in-
result in a different payout or recipient from the contract. vestors to lose all Ether invested in the contract. Similar
Reentrancy Handling. Oyente reports 340 instances of attacks exist in other contracts as well (see [22, 25]).
this vulnerability, out of which 186 are distinct. Only 2 of Manipulation of contract outcome. PonziGovernMen-
these have source code available, one of which is the infa- tal is another example of timestamp-dependent contract.
mous TheDAO contract [19]. The other known-source con- In Line 5, PonziGovernMental determines the current time
tract has reentrancy vulnerability, but the vulnerability is by using the current block timestamp. If a user invokes
not exploitable since it uses the SEND instruction instead of PonziGovernMental when it is close to 12 hours since the last
a CALL to call to a different account. The significant differ- deposit, the miner can set the next block timestamp to make
ence here is that a CALL sends all of the remaining gas to the condition in Line 5 either valid or invalid. Thus, min-
the callee at the time it is made, whereas a SEND limits this ers can force the PonziGovernMental contract to finish the
amount. This simple change would limit the damage from current round earlier by picking a timestamp value which is
possible reentrancy attack. We further test Oyente on a ahead of the current time. Alternatively, miners can extend
number of publicly available reentrancy examples [36] [37], the round for 12 hours by choosing a smaller timestamp.
and Oyente confirms all cases where repeated execution of Thus, miners who have a stake in the contract will set the
a call was possible. timestamp to a value which favors their outcome. The prob-
lem also exists in other contracts (see [28]).
6.3 Qualitative Analysis
Lock or Sabotage Others’ Funds. Attackers can also
We investigate several contracts flagged by Oyente to prevent others from receiving their legitimate payments. One
show how it helps analyze Ethereum smart contracts. example of such an attack is in EtherID, which is one of the
most active contracts in Ethereum with 57, 738 received/sent
6.3.1 Severity of Attacks transactions as of writing [38]. EtherID works as a name
We have found vulnerable contracts which have differ- registrar for Ethereum network to allow users to create, buy
ent levels of damage severity reported in Section 6.2. For and sell any ID (like a token). The code which handles
instance, the PonziGovernMental [26] contract with highest users’ requests to buy a registered ID is in Figure 18. The
balance (1, 099.5 Ether) flagged by Oyente among the mis- code checks if the buyer has enough Ethers (Line 2), sends
handled exception category. The contract operates as below. the payment to the existing owner (Line 4) and change the
• The contract accepts investments from users. New invest- ownership of the ID (Line 5–10). As described in Section 3.3,
ments pay to previous investors and add to the jackpot. the send instruction in Line 4 may fail. As a result, the ID

265
 1 contract Foo { 1 function l e n d G o v e r n m e n t M o n e y ( address buddy )
2 Foo public self ; 2 returns ( bool ) {
3 EtherId public etherid ; 3 uint amount = msg . value ;
4 uint256 public domain ; 4 // check the condition to end the game
5 /../ 5 if ( l a s t T i m e O f N e w C r e d i t + TWELVE_HOURS >
6 function callself ( int counter ){ 6 block . timestamp ) {
7 if ( counter < 1023){ 7 msg . sender . send ( amount );
8 if ( counter > 0) 8 // Sends jacpot to the last creditor
9 self . callself . gas ( msg . gas -2000)( counter +1); 9 c r e d i t o r A d d r e s s e s [ c r e d i t o r A d d r e s s e s . length - 1]
10 else self . callself ( counter +1); 10 . send ( pro fitF rom Cras h );
11 } 11 owner . send ( this . balance );
12 else etherid . changeDomain . value ( this . balance )\ 12
13 ( domain , 10000000 , 1 ether /100 , 0); 13 // Reset contract state
14 }} 14 l a s t C r e d i t o r P a y e d O u t = 0;
Figure 16: A contract conducts the call-stack attack by calling 15 l a s t T i m e O f N e w C r e d i t = block . timestamp ;
16 pr ofit From Cras h = 0;
itself 1023 times before sending a buy request to EtherID. 17 c r e d i t o r A d d r e s s e s = new address [](0);
18 cr edit orAm ount s = new uint [](0);
19 round += 1;
20 return false ;
owners may not receive the payment and still have to trans- 21 }}
fer the ownership of their ID to the buyers. There is no way
Figure 17: PonziGovernmentMental contract, with over 1000
for the owners to claim the payment later on. The Ether Ether, allows users to participate/profit from the creation/fall
value is locked in the contract forever. of a government.

6.4 Public Verification

Verifying the above attack on the public blockchain is fea- Scissors”) can contain several logic problems, including:
sible, but for ethical reasons we do not conduct our attack • Contracts do not refund. Some contracts proceed further
confirmation on contracts [22, 25, 26] where users may lose only if users send a certain amount of Ether. However,
funds. Instead, we perform our verification on EtherID con- these contracts sometimes “forget” to refund users if users
tract on which the attack has less severity. More impor- send less than what is required.
tantly, EtherID allows us to target our own accounts, other
accounts are not affected in the experiments. • Lack of cryptography to achieve fairness. Some contracts
We verify the problem of EtherID by creating our own IDs perform computation based on users’ inputs to decide the
and self-purchasing them. We show that the registers of our outcome (e.g., rolling a die). However, those contracts
IDs do not receive the intended payments when the registers store users’ input in plaintext on the blockchain. Thus,
use contract wallets, or when the buyers are malicious and malicious users can submit inputs biased in their favor.
conduct the call-stack exceeding attack. • Incentive misalignment. Some contracts do not incen-
Our two IDs are dummywallet and foowallet registered by tivize users to follow intended behavior. Consider a gam-
two addresses 0x33dc532ec9b61ee7d8adf558ff248542c2a2a62e bling game that uses a commit-reveal scheme in which
and 0x62ec11a7fb5e35bd9e243eb7f867a303e0dfe08b respectively. participants first submit their encrypted move along with
The price to buy either of the ID is 0.01 Ether. The address a deposit before later revealing it. After the first move is
0x33dc532... is a contract address, which performs some revealed, the second user may realize his move will lose.
computation (thus burning gas) on receiving any payment. Since his deposit lost, he may not be willing to spend gas
We then send two transactions from different addresses to to reveal his choice.
buy the two IDs. The first transaction 6 purchases dummy- These security problems are more about logical flaws in the
wallet. However, 0x33dc532... is a contract address, which is implementation of contracts. In contrast, our paper docu-
implemented to burn all the provided gas on receiving any ments new security bugs stemming from semantic misunder-
payment without doing anything else. Thus the send func- standings of smart contract developers. We suggest improve-
tion in Line 4 of EtherID to 0x33dc532... will fail. As a result, ments to the semantics and introduce Oyente to detect
0x33dc532... sells it ID without receiving any payment. The these bugs in existing contracts in the Ethereum blockchain.
fund 0.01 Ethers is kept in the contract EtherID forever. Our evaluation showed that 8, 519 existing contracts con-
The second transaction 7 sent from a contract, which calls tain at least one of the new bugs. The call-stack problem
itself 1023 times before sending a buy request to EtherID to of Ethereum was reported previously in a security audit by
buy foowallet. The code snippet to perform such attack is Miller et al. [24]. The bug, however, still remains unfixed.
in Figure 16. When EtherID executes send in Line 4, the Other work also studies security and/or privacy concerns
call stack already has 1024 frames, so send fails regardless in designing smart contracts [6, 27, 39, 40]. For instance,
of how much gas is used. Hence, the address 0x62ec11a7... Hawk [27] provides confidential execution for contracts by
does not receive the payment of 0.01 Ethers as it should. leveraging cryptographic techniques and Town Crier [39]
feeds reliable, trustworthy data from trusted web servers to
7. RELATED WORK smart contracts via hardware rooted trust.
Distributed Systems and Programming Languages.
Smart Contract Security. Delmolino et al. [14] show that Security problems in smart contracts are often related to
even a simple self-construct contract (e.g., “Rock, Paper, problems in traditional distributed systems. For example,
6
TX hash: 0xb169b07c274a71727ecfe9d0610d09917c45- concurrency control in multiuser distributed database sys-
4c1216cd659350f83ef44ba071b4 tems (DBMS) [41] is superficially similar to the transaction-
7 order dependency problem. However, transaction-ordering
TX hash: 0x0c10fafe0cdbfff32abfe53d57ec861d09-
986cc1050c850481f79b1a862bb10a problems in permissionless distributed systems like cryp-

266
 1 // ID on sale , and enough money [9] Counterparty platform. http://counterparty.io/, 2015.
2 if ( d . price > 0 && msg . value >= d . price ){ [10] James C. Corbett, Jeffrey Dean, Michael Epstein,
3 if ( d . price > 0)
4 address ( d . owner ). send ( d . price );
Andrew Fikes, Christopher Frost, J. J. Furman, Sanjay
5 d . owner = msg . sender ; // Change the ownership Ghemawat, Andrey Gubarev, Christopher Heiser,
6 d . price = price ; // New price Peter Hochschild, Wilson Hsieh, Sebastian Kanthak,
7 d . transfer = transfer ; // New transfer
8 d . expires = block . number + expires ;
Eugene Kogan, Hongyi Li, Alexander Lloyd, Sergey
9 DomainChanged ( msg . sender , domain , 0 ); Melnik, David Mwaura, David Nagle, Sean Quinlan,
10 } Rajesh Rao, Lindsay Rolig, Yasushi Saito, Michal
Figure 18: EtherID contract, which allows users to register, buy Szymaniak, Christopher Taylor, Ruth Wang, and Dale
and sell any ID. This code snippet handles buy requests from Woodford. Spanner: Google’s globally distributed
users. database. ACM Trans. Comput. Syst., aug 2013.
[11] Jason Baker, Chris Bond, James C. Corbett,
tocurrencies are more complex than in traditional systems JJ Furman, Andrey Khorlin, James Larson,
because adversaries can manipulate the order. Jean-Michel Leon, Yawei Li, Alexander Lloyd, and
Many previous works attempt to build a global times- Vadim Yushprakh. Megastore: Providing scalable,
tamp in distributed systems, in both asynchronous and syn- highly available storage for interactive services. In
chronous settings [42–44]. Time in distributed systems tra- Proceedings of the Conference on Innovative Data
ditionally forms a partial order rather than the the total system Research (CIDR), pages 223–234, 2011.
order given by the blockchain. As we discussed in Section 3, [12] KingOfTheEtherThrone smart contract. https:
having access to the block timestamp (in addition to the //github.com/kieranelby/KingOfTheEtherThrone/
block id) is redundant and invites attack. Lastly, propagat- blob/v0.4.0/contracts/KingOfTheEtherThrone.sol.
ing exceptions is inspired by the exception handling mecha- [13] GovernMental’s 1100 ETH payout is stuck because it
nism in modern languages [45, 46]. uses too much gas. https:
//www.reddit.com/r/ethereum/comments/4ghzhv/
8. ACKNOWLEDGMENT governmentals 1100 eth jackpot payout is stuck/.
We thank Brian Demsky, Vitalik Buterin, Yaron Welner, [14] Kevin Delmolino, Mitchell Arnett, Ahmed Kosba,
Gregory J. Duck, Christian Reitwiessner, Dawn Song, An- Andrew Miller, and Elaine Shi. Step by step towards
drew Miller, Jason Teutsch, Alex Zikai Wen, Patrick Cousot creating a safe smart contract: Lessons and insights
and Joseph Chow for useful discussions and feedback on the from a cryptocurrency lab. Cryptology ePrint Archive,
early version of the paper. This work is supported by the Report 2015/460, 2015. http://eprint.iacr.org/.
Ministry of Education, Singapore under Grant No. R-252- [15] Gavin Wood. Ethereum: A secure decentralised
000-560-112 and in part by Yale-NUS College under Grant generalised transaction ledger.
No. R-607-265-045-121. All opinions expressed in this work http://gavwood.com/paper.pdf, 2014.
are solely those of the authors. [16] Ethereum Foundation. The solidity contract-oriented
programming language.
9. REFERENCES https://github.com/ethereum/solidity.
[1] Satoshi Nakamoto. Bitcoin: A peer-to-peer electronic [17] Ethereum Foundation. The serpent contract-oriented
cash system. bitcoin.org, 2009. programming language.
[2] Ethereum Foundation. Ethereum’s white paper. https: https://github.com/ethereum/serpent.
//github.com/ethereum/wiki/wiki/White-Paper, [18] Oyente project page.
2014. https://www.comp.nus.edu.sg/˜loiluu/oyente.html.
[3] A Miller, A Juels, E Shi, B Parno, and J Katz. [19] TheDAO smart contract. http://etherscan.io/address/
Permacoin: Repurposing Bitcoin work for long-term 0xbb9bc244d798123fde783fcc1c72d3bb8c189413#code.
data preservation. IEEE Security and Privacy, 2014. [20] EtherEx: A fully decentralized cryptocurrency
[4] Use case for factom: The world’s first blockchain exchange. https://etherex.org/.
operating system (bos). http://kencode.de/projects/ [21] EtherOpt: A decentralized options exchange.
ePlug/Factom-Linux-Whitepaper.pdf, Feb 2015. http://etheropt.github.io/.
[5] Nick Szabo. The idea of smart contracts. [22] The Run smart contract.
http://szabo.best.vwh.net/smart contracts idea.html, https://etherscan.io/address/
1997. 0xcac337492149bdb66b088bf5914bedfbf78ccc18.
[6] Loi Luu, Jason Teutsch, Raghav Kulkarni, and [23] Ethereum Foundation. Block validation algorithm.
Prateek Saxena. Demystifying incentives in the https://github.com/ethereum/wiki/wiki/Block-
consensus computer. In Proceedings of the 22Nd ACM Protocol-2.0#block-validation-algorithm.
SIGSAC Conference on Computer and [24] Andrew Miller, Brian Warner, and Nathan Wilcox.
Communications Security, CCS ’15, pages 706–719. Gas economics. https://github.com/LeastAuthority/
ACM, 2015. ethereum-analyses/blob/master/GasEcon.md.
[7] EtherDice smart contract is down for maintenance. [25] Protect The Castle Contract.
https: http://protect-the-castle.ether-contract.org/.
//www.reddit.com/r/ethereum/comments/47f028/ [26] GovernMental Smart Contract.
etherdice is down for maintenance we are having/. http://governmental.github.io/GovernMental/.
[8] RSK Labs. Rootstock: Smart contracts platform
powered by Bitcoin. http://www.rootstock.io/, 2015.

267
[27] Ahmed Kosba, Andrew Miller, Elaine Shi, Zikai Wen, http://vessenes.com/more-ethereum-attacks-race-to-
and Charalampos Papamanthou. Hawk: The empty-is-the-real-deal/.
blockchain model of cryptography and [38] Alexandre Naverniouk. EtherID: Ethereum name
privacy-preserving smart contracts. In Proceedings of registrar. http://etherid.org/.
the 2016 IEEE Symposium on Security and Privacy, [39] Fan Zhang, Ethan Cecchetti, Kyle Croman, Ari Juels,
SP ’16. IEEE Computer Society, 2016. and Elaine Shi. Town crier: An authenticated data
[28] Lottopolo smart contract. feed for smart contracts. Cryptology ePrint Archive,
https://etherchain.org/account/ Report 2016/168, 2016. http://eprint.iacr.org/.
0x0155ce35fe73249fa5d6a29f3b4b7b98732eb2ed. [40] Ari Juels, Ahmed Kosba, and Elaine Shi. The ring of
[29] Random number generator contract. Gyges: Investigating the future of criminal smart
https://github.com/randao/randao. contracts. Cryptology ePrint Archive, Report
[30] Joseph Bonneau, Jeremy Clark, and Steven Goldfeder. 2016/358, 2016. http://eprint.iacr.org/.
On Bitcoin as a public randomness source. Cryptology [41] Philip A. Bernstein and Nathan Goodman.
ePrint Archive, Report 2015/1015, 2015. Concurrency control in distributed database systems.
http://eprint.iacr.org/. ACM Comput. Surv., 13(2):185–221, June 1981.
[31] James C. King. Symbolic execution and program [42] Friedemann Mattern. Virtual time and global states of
testing. Commun. ACM, 19(7):385–394. distributed systems. In Parallel and Distributed
[32] Patrick Cousot and Radhia Cousot. Abstract Algorithms, pages 215–226. North-Holland, 1989.
interpretation: A unified lattice model for static [43] C. J. Fidge. Timestamps in message-passing systems
analysis of programs by construction or approximation that preserve the partial ordering. Proceedings of the
of fixpoints. In Proceedings of the 4th ACM 11th Australian Computer Science Conference,
SIGACT-SIGPLAN Symposium on Principles of 10(1):56âĂŞ66, 1988.
Programming Languages, pages 238–252, New York, [44] Leslie Lamport. Time, clocks, and the ordering of
NY, USA, 1977. ACM. events in a distributed system. Commun. ACM, pages
[33] Microsoft Corporation. The Z3 theorem prover. 558–565, July 1978.
https://github.com/Z3Prover/z3. [45] Andrew Koening and Bjarne Stroustrup. Exception
[34] The Ethereum block explorer. https://etherscan.io/. handling for C++. Journal of Object-Oriented
[35] The Ethereum network stats. https://etherchain.org/. Programming, 3(2):16–33, 1990.
[36] Peter Borah. Tokenwith invariants - vulnerable [46] Robin Milner, Mads Tofte, and David MacQueen. The
contracts in ethereum. https://github.com/ Definition of Standard ML. MIT Press, Cambridge,
PeterBorah/smart-contract-security-examples/blob/ MA, USA, 1997.
7d7ef27b12f15318871c44512b70737176d23c5f/
contracts/TokenWithInvariants.sol. APPENDIX
[37] Peter Vessenes. More ethereum attacks: Table 2 describes the operational semantics of EtherLite.
Race-to-empty is the real deal.

268
 Table 2: Operational Semantics of EtherLite. EXC stands for “Exception”.

M [pc] Conditions µ µ0
push v hhM, pc, l, si · A, σi hhM, pc + 1, l, v · si · A, σi
pop hhM, pc, l, v · si · A, σi hhM, pc + 1, l, si · A, σi
op op: unary operator and v 0 ← op v hhM, pc, l, v · si · A, σi hhM, pc + 1, l, v 0 · si · A, σi
op op: binary operator and v 0 ← v1 op v2 hhM, pc, l, v1 · v2 · si · A, σi hhM, pc + 1, l, v 0 · si · A, σi
bne z=0 hhM, pc, l, • · z · si · A, σi hhM, pc + 1, l, si · A, σi
bne z 6= 0 and λ is a valid target hhM, pc, l, λ · z · si · A, σi hhM, λ, l, si · A, σi
bne z 6= 0 and λ is NOT a valid target hhM, pc, l, λ · z · si · A, σi hheiexc · A, σi
mload v ← l[i] hhM, pc, l, i · si · A, σi hhM, pc + 1, l, v · si · A, σi
mstore l0 ← l[i 7→ v] hhM, pc, l, i · v · si · A, σi hhM, pc + 1, l0 , si · A, σi
id ← address of the executing contract
sload hhM, pc, l, i · si · A, σi hhM, pc + 1, l, v · si · A, σi
v ← σ[id][i]
id ← address of the executing contract
sstore hhM, pc, l, i · v · si · A, σi hhM, pc + 1, l, si · A, σ 0 i
σ 0 ← σ[id][i 7→ v]
id ← address of the executing contract
a0 ← hM, pc, l, si
call M 0 ← Lookup(σ, γ) hhM, pc, l, γ · z · st · sz · si · A, σi hhM 0 , 0, l0 , i · a0 · A, σ 00 i
σ 0 ← σ[id][bal 7→ σ[id][bal] − z]
σ 00 ← σ 0 [γ][bal 7→ σ[id][bal] + z]
id ← address of the executing contract
call hhM, pc, l, • · v · • · • · • · • · si · A, σi hhM, pc + 1, l, 0 · si · A, σi
σ[id][bal] < v or |A| = 1023
return hhM, pc, •, •i · , σi h, σi
a0 ≡ hM 0 , pc0 , l00 , st0 · sz 0 · s0 i
return n ← min(sz 0 , sz) hhM, pc, l, st · sz · si · a0 · A, σi hhM 0 , pc0 + 1, ln0 , 1 · s0 i · A, σi
0
0 ≤ i < n : li+1 ← li0 [st0 + i 7→ l[st + i]]
EXC exceptional halting of callee hheiexc · hM, pc, l, st · sz · si · A, σi hhM, pc + 1, l, 0 · si · A, σi
id ← address of the executing contract
σ 0 ← σ[γ][bal 7→ (σ[γ][bal] + σ[id][bal])]
suicide hhM, pc, •, γ · si · , σi h, σ 00 i
σ 00 ← σ 0 [id][bal 7→ 0]
Register id for later deletion
id ← address of the executing contract
a0 ≡ hM 0 , pc0 , l00 , • · • · s0 i
suicide σ 0 ← σ[γ][bal 7→ (σ[γ][bal] + σ[id][bal])] hhM, pc, •, γ · si · a0 · A, σi hhM 0 , pc0 + 1, ln0 , 1 · s0 i · A, σi
σ 00 ← σ 0 [id][bal 7→ 0]
Register id for later deletion

269