Automated Security Analysis of Ethereum Smart Contracts

With uncountable projects using smart contracts based on the blockchain technology racing to market, there is an ever-growing need for safe contracts to protect what could potentially be worth billions.

How do we get to those needed safety standards while keeping speed and efficiency within these projects up? In this post we are evaluating on the advantage or necessity to include static formal verifications into a smart contract development and audit process.

Overview

The Ethereum blockchain is a decentralized platform that supports the execution of arbitrary, Turing-complete programs, known as smart contracts. Smart contracts have been shown to simplify many processes by cutting out intermediaries and are praised for supporting a wide range of applications, including those found in the financial (e.g., decentralized insurances, trade clearing), the public sector (record-keeping) and the cross-industry (peer-to-peer trading) domains.

While promising, Turing-complete languages leave room for critical vulnerabilities, which are discovered and exploited by attackers every few months. In this article, we first motivate the importance of smart contract security and present a simple, yet illustrative example that shows a subtle security flaw in a popular smart contract. Afterwards, we explore the space of possible solutions to automated discovery of security issues in smart contracts (including testing, dynamic, and static analysis) and discuss their limitations.

The need for strong security guarantees

The role of security in the context of smart contracts cannot be understated: Smart contracts must be free of security vulnerabilities.

On the one hand, developers must ensure that attackers cannot steal the money stored at their contracts. On the other hand, users interacting with a contract implicitly trust the smart contract. Namely, they trust that the money they invest/deposit in a smart contract is securely handled and will not end up in the hands of attackers.

The first example that made the news and shook the trust in smart contracts is the famous attack on the DAO contract: In June 2016, the DAO contract had received more than $150 million investment from more than 11,000 investors. The security of the DAO contract was compromised, which enabled an attacker to steal over $50 million. Following this attack, in July 2017, a security bug in a popular wallet contract allowed an attacker to steal $30 million. Four months later, in early November 2017, another critical vulnerability was discovered in the very same smart contract, freezing all funds stored in a number of wallets, affecting nearly $280 million. It has become apparent that writing secure smart contracts is a significant challenge.

Writing secure smart contracts is not easy

Developers struggle in writing smart contracts that are secure. One reason is that the high-level languages for writing smart contracts are seemingly close to standard programming languages. However, the underlying semantics of the blockchain are radically different and often surprise developers. To illustrate this point, consider the following smart contract:

contract SimpleBank { 
  mapping(address => uint) balances;
  function deposit(uint amount) { 
    balances[msg.sender] += amount;
  }
  function withdraw() { 
    msg.sender.call.value(balances[msg.sender])();
    balances[msg.sender] = 0;
  }
}

This contract enables users to deposit ether (the currency used within Ethereum). Further, it allows users to withdraw all their deposited ether by making a call to method withdraw. In this method, the instruction call triggers a transfer of ether from the SimpleBank contract to the transaction sender. However, the method call has a subtle behavior: it transfers control over the execution to the transaction sender (which can be another contract). Since the balance is not zeroed at the time control is handed to the transaction sender, a malicious contract can invoke withdraw again to drain more money from the SimpleBank contract. An attacker can exploit this vulnerability to drain all the ether deposited in the contract.

Understanding and foreseeing this vulnerability requires a deep understanding of the blockchain platform. This security flaw was overseen by developers, allowing an attacker to steal $50 million from the infamous DAO contract.

Is it possible to find security vulnerabilities in smart contracts automatically?

To avoid tremendous financial losses due to security bugs in smart contracts, we would ideally construct an algorithm that automatically finds security issues in smart contracts. Unfortunately, such an algorithm does not (and cannot) exist. Smart contracts are written in Turing-complete languages, such as Solidity, which intuitively means that one can capture any computation in these languages. It is well-known that it is impossible to construct an algorithm that takes as input an arbitrary program (written in a Turing-complete language) together with an arbitrary property (e.g. “the contract is free of the DAO vulnerability”) and returns yes, if the program satisfies the property and no, if the program violates the property.

This implies that we cannot have an algorithm that precisely detects security vulnerabilities in smart contracts. This may sound discouraging, but there are techniques that can help developers check the security of their smart contracts.

3 Techniques for automated analysis of smart contracts

To gain confidence in the correctness and security of normal programs, developers usually turn to testing, dynamic analysis, and static analysis. Three techniques vastly differ in the guarantees they provide. To illustrate these differences, one can think of the semantics of a smart contract as the set of all possible behaviors that it can exhibit. Intuitively, each behavior corresponds to running the contract in a given state and with a given input (e.g. transaction data). Visually, the behaviors of a smart contract can be represented as follows:

The blue zone delimits the set of all possible behaviors of the contract. Some of these behaviors exhibit bugs (i.e., security issues). Developers would like to discover those. We remark that the set of all possible contract behaviors is enormous. It is impossible to enumerate them and check them individually for bugs.

1. Finding bugs in contracts using testing

Testing is like shooting with a pistol: you have to hit the bug in order to find it.

A single test checks a single behavior. So, unless you have a test that exposes the bug, the bug would remain uncovered. Today, there are many techniques that can help developers to generate tests in an automated manner, e.g. using fuzzing. However, it is hard to gain strong confidence on the security of a contract using testing, simply because the vast majority of the behaviors remain unexplored.

2. Checking smart contracts using dynamic analysis

Dynamic analysis is more like shooting with a shotgun: once the bullet strikes, it damages an entire area instead of a single point.

Dynamic analysis techniques leverage symbolic reasoning to generalize the guarantees obtained by observing a single behavior to guarantees that hold for a set of behaviors. For example, dynamic analysis can observe an execution and use symbolic reasoning to generalize that an integer variable would not overflow for all behaviors that execute the same sequence of instructions. Unfortunately, it is difficult, and even impossible in the presence of unbounded loops, to explore all behaviors by dynamic analysis. Bugs, therefore, will remain undiscovered.

3. Formal verification of smart contracts using static analysis

Verification using static analysis is like a bomb: once it hits the ground, it hits everything around it.

The goal of static analysis is to automatically inspect the source code of a smart contract and to over-approximate all possible behaviors of the contract. Correctly over-approximating the semantics of smart contracts can be quite challenging, and requires an in-depth knowledge systematic analysis approaches (e.g. abstract interpretation) and the blockchain execution semantics. The reward of getting this correctly is that if a given bug (e.g. transaction reordering) is not found during the analysis, then all behaviors of the smart contract are free of this bug.

What to use?

In the context of smart contract security, it is important to not miss any security issues. If Static analysis reports that a contract is free of certain vulnerabilities, then the contract is indeed secure against them. On the contrary, if the analysis reports a potential issue, then it may or may not be exploitable by an attacker. A security expert is thus needed to carefully inspect the potential issues and to check whether they can occur at runtime.

For this reason, ChainSecurity is developing and using static analysis as the foundation of all our audits, followed up by security expert know-how. For example, the founders of ChainSecurity have previously developed Securify, the first automated formal verifier for Ethereum smart contracts. Get in touch if you share our goal to provide the best security tools around smart contract development!