Summary – Making smart contracts smarter

As part of my research into smart contract verification, I am going to be reviewing publications in this field. This is a summary of the technical paper “Making smart contracts smarter”.

Smart contracts (or contracts) are lines of code that get deployed on blockchain and are executed automatically when certain conditions are met. Due to the inherent feature of immutability in blockchain, once deployed, the contract code cannot be modified. It needs to be re-deployed to a new address location on the chain. Hence, designing and development have to be considered carefully.

Over the past few years, we have seen a lot of security issues with smart contracts, mainly in Ethereum, due to which millions of dollars have been lost or hacked. This is mainly due to the gaps in the understanding of the operational semantics of the underlying platform like EVM (Ethereum Virtual Machine).

In this paper, the authors analyze existing Ethereum smart contracts and identify various types of security concerns due to the current distributed setting. They propose new operational semantics which would help diagnose these issues dynamically. To implement and enforce these semantics would require a hard fork and upgrade of all the clients in the network. Hence, an open-source tool called — Oyente is also provided, which uses symbolic execution to associate any of the paths in the code that might lead to the listed vulnerabilities.

Security Flaws in Contracts

Transaction-Ordering Dependence (TOD)

A miner who is creating a block has control over which transactions are included and also the order of the transactions. Thus, the state updates in blockchain are mainly determined by the miners.

Attacks: 

1. Concurrent invocations in a blockchain can yield different results even for a benign user.
2. Malicious users can gain profits by exploiting the TOD contracts and steal user’s money. Ex: Payouts dependent on the order of transactions.

Timestamp Dependence 

This the case when block timestamp is used for executing a critical condition in a smart contract. Ex: Sending money. Such contracts are called timestamp-dependence contracts. When a miner creates a block, he needs to set a timestamp on the block. This the local timestamp of the miner’s system, which can be tampered with by the miner. The maximum variation allowed in timestamp between miners is 900 seconds. This variation can instill a lot of discrepancies in the timestamp-dependent contracts.

Mishandling Exceptions 

In solidity, there are few ways to make calls between smart contracts, e.g., via send or call instruction. With these calls, if there is any exception the state changes are reverted and they return false. On the caller side, this needs to be checked in order to handle these exceptions. If not, the execution moves forward even though the send instruction has returned an exception. Below is an example for the same.

Attacks:

1. Exceeding call-stack depth limit – Ethereum Virtual Machine (EVM) limits call-stack depth to 1024 frames. It increases by one if a call to another contract is made using send. This can be used by malicious user to forcefully exceed the call-stack depth causing an exception.

Reentrancy Vulnerability 

A well-known and well-studied vulnerability due to the DAO hack, where the attacker exploited the reentrancy vulnerability to steal over 3,600,000 Ether, or 60 million US Dollars at the time of the attack. This is caused due to the use of intermediate state by the callee contract during a function call between smart contracts.

Workaround for Vulnerabilities

Authors propose various operational semantics that could be included in EVM implementation to avoid all the mentioned attacks. Some of the semantics cover:

• Formation and validation of a block
• Transaction execution
• Guarded Transactions for TOD
• Using block index instead of timestamp
• Explicit throw and catch instructions in EVM for handling exceptions.

The Oyente Tool

All of the solutions above require a hard fork of the blockchain, which might be a hassle. Hence, authors went with a pre-deployment option; creating a tool that developers can use to test the smart contracts before they are deployment on a blockchain.

Symbolic execution represents the values of program variables as symbolic expressions of the input symbolic values. Each symbolic path has a path condition which is a formula over the symbolic inputs built by the accumulating constraints which those inputs must satisfy in order for the execution to follow that path. A path is infeasible if its path condition is unsatisfiable. Otherwise, the path is feasible. 

Oyente is based on symbolic execution as it can statically reason about a program path-by-path. In Ethereum, it is very difficult to accomplish dynamic testing, given the non-determinism and complexity of blockchain behaviour.

The tool takes two inputs – bytecode of a contract and current Ethereum global state. The output gives any problematic paths. The execution also involves creating a Control Flow Graph (CFG) of the contract code which is fed to a Graph Visualizer. Oyente follows a modular design. It has four main components:

• CFGBuilder – Builds the CFG for contracts code.
• Explorer – Symbolically executes the contract.
• CoreAnalysis – All of the suggested semantical logic is implemented here. Output of Explorer is pushed to this module to verify for any of the vulnerabilities discussed.
• Validator – Filters out some false positives before reporting to the users.

Implementation

Oyente is implemented in python with roughly 4,000 lines of code. Z3 solver is used for checking the satisfiability of the code.

Evaluation

Around 19,366 smart contracts with a total balance of 3,068,654 Ether, or 30 Million US Dollars were collected from the blockchain as of May 5, 2016. Both quantitative and qualitative analysis has been performed on these smart contracts using Oyente. The tool exhibits a low false-positive rate of 6.4%, i.e., only 10 cases out of 175.