Smart Contract Analysis

sCompile: Critical Path Identification and Analysis for Smart Contracts

Built on top of cryptographic algorithms and the blockchain technology, cryptocurrency like Bitcoin has been developing rapidly in recent years. Many believe that it has the potential to revolutionize the banking industry by allowing monetary transactions in an anonymous, distributed, and trusted way. Smart contracts bring it one step further by providing a framework which allows any contract (not only monetary transactions) to be executed in an autonomous, distributed, and trusted way. Smart contracts thus may revolutionize many industries. Ethereum, an open-source, blockchain-based cryptocurrency, is the first to integrate the functionality of smart contracts. Due to its enormous potential, the price of Ethereum has increased 5464.71% since Jul 30th, 2015 and the market cap reached at $45.13B as of Nov 28th, 2017.

In essence, smart contracts are computer programs which are automatically executed on a distributed blockchain infrastructure. Popular applications of smart contracts include crowd fund raising and online gambling, which often involve monetary transactions as part of the contract. Smart contracts in Ethereum are written in a programming language called Solidity. Like traditional programs, smart contracts written in Solidity may contain vulnerabilities, which potentially lead to attacks. The problem is magnified by the fact that smart contracts, unlike ordinary programs, cannot be patched once they are deployed on the blockchain.

In recent years, there have been an increasing number of news reports on attacks targeting smart contracts. These attacks exploit security vulnerabilities in Ethereum smart contracts and often result in stolen money. One notorious example is the DAO attack, i.e., an attacker stole more than 3.5 million Ether (which was equivalent to about $45 million USD at the time) from the DAO contract on June 17, 2017. This attack is carried out through a bug in the DAO contract (i.e., in the splitDAO function). The correctness and systematic analysis of smart contracts since then have been brought into sight with urgency.

There have been multiple attempts on building tools which aim to analyze smart contracts fully automatically. For instance, the tool named Oyente applies symbolic execution techniques to find potential security vulnerabilities in Solidity smart contracts. For another instance, the tool named MAIAN analyzes smart contracts against three trace properties through symbolic execution.

The problem of analyzing and verifying smart contracts is far from being solved. Some believe that it will never be, just as the verification problem of traditional programs. Solidity is designed to be Turing-complete which intuitively means that it is very expressive and flexible. The price to pay is that almost all interesting problems associated with checking whether a smart contract is vulnerable are undecidable. Consequently, tools which aim to analyze smart contracts automatically either are not scalable or produce many false alarms. For instance, Oyente is designed to check whether a program path leads to a vulnerability or not using a constraint solver to check whether the path is feasible or not. Due to the limitation of constraint solving techniques, if Oyente is unable to determine whether the path is feasible or not, the choice is either to ignore the path (which may result in a false negative, i.e., a vulnerability is missed) or to report an alarm (which may result in a false alarm).

We develop a powerful approach for analyzing smart contracts. We believe that manual inspection is unavoidable given the expressiveness of Solidity. However, given that smart contracts often enclose many behaviors (which manifest through different program paths), manually inspecting every program path is simply overwhelming. Thus, our goal is to reduce the manual effort by identifying a small number of critical program paths and presenting them to the user with easy-to-digest information. Towards this goal, we make the following contributions.

  • We develop a tool called sCompile which can systematically enumerate all possible program paths including those due to the fallback function. Given a smart contract, sCompile constructs a control flow graph (CFG) which captures all possible control flow. Based on the CFG, we can systematically generate program paths which are constituted by a bounded sequence of function calls (including the fallback function).
  • As the number of program paths are often huge, sCompile then statically identifies the critical paths which manual inspection should focus on. We define paths which involve monetary transaction as critical paths. Focusing on such paths allows us to “follow the money”, which is often sufficient in capturing vulnerabilities in smart contracts.
  • Afterwards, to prioritize the program paths, sCompile analyze each of them to see whether it potentially violates certain critical property. We define a set of (configurable) money-related properties based on existing vulnerabilities. After the analysis, sCompile then ranks the program paths by computing a criticalness score for each program path. The criticalness score is calculated using a formula which takes into account what properties the program path potentially violates and its length (so that a shorter path is more likely to be presented for user inspection).
  • Next, for each program path which has a criticalness score larger than a threshold, sCompile automatically checks whether it is feasible using symbolic execution techniques. The idea is to automatically filter those infeasible if possible to reduce user effort.
  • Lastly, the remaining critical paths with a criticalness score larger than a threshold are presented to the user for user inspection through an interactive user interface.

sCompile is implemented in C++ and has been applied systematically to more than 30 thousand smart contracts which are gathered from EtherScan. Our experiment results show that sCompile can efficiently analyze smart contracts, i.e., it spends 5 seconds on average to analyze a smart contract. This is mainly because sCompile is designed to rank the program paths based on static analysis and only applies symbolic execution to critical (monetary) paths, which significantly reduces the number of times symbolic execution is applied. Furthermore, we show that sCompile effectively prioritizes programs paths which reveal vulnerabilities in the smart contracts, i.e., it is often sufficient to capture the vulnerability by inspecting the reported 10 or fewer critical program paths. Lastly, using sCompile, we identify 71 previously unknown vulnerabilities in three days. We further conduct a user study which shows that with sCompile’s help, users are significantly more likely to identify vulnerabilities in smart contracts.

Illustrative Examples

In the following, we present multiple examples to illustrate vulnerabilities in smart contracts and how sCompile helps to reveal them.

Example 1

contract EnjinBuyer {
       address public developer = 0x0639C169D9265Ca4B4DEce693764CdA8ea5F3882;
       address public sale = 0xc4740f71323129669424d1Ae06c42AEE99da30e;

       function purchase_tokens() {
              require(msg.sender == developer);
              contract_eth_value = this.balance;
              require(sale.call.value(contract_eth_value)());
              require(this.balance==0);
       }
}

Contract EnjinBuyer is a token managing contract. It has 2 inherent addresses for developer and sale. In function purchase_tokens(), the balance is sent to the sale’s address. There is a mistake on the sale’s address and as a result the balance is sent to a non-existing address and is lost forever. Note that any hexadecimal string of length not greater than 40 is considered a valid (well-formed) address in Ethereum and thus there is no error when function purchase_tokens() is executed.

Given this contract, the most critical program path reported by sCompile is one which invokes function purchase_tokens(). The program path is labeled with a message stating that the address does not exist on Ethereum mainnet. With this information, it is easy to capture the vulnerability. We remark that there are no existing tools which check such vulnerability.

Example 2

contract toyDAO{
       address owner;
       mapping (address => uint) credit

       function toyDAO() payable public {
              owner = msg.sender;
       }

       function donate() payable public{
              credit[msg.sender] = 100;
       }

       function withdraw() public {
              uint256 value = 20; //line 0
              if (msg.sender.call.value(value)()) { //line 1
                     credit[msg.sender] = credit[msg.sender] – value; //line 3
              }
       }
}

Contract toyDAO is a simple contract which has the same problem of the DAO contract. Mapping credit is a map which records the amount associated with a user. Function donate() allows a user to top up its account with 100 wei (which is a unit of Ether). Function withdraw() by design sends 20 wei to the message sender (at line 1) and then updates credit accordingly. However, when line 1 is executed, the message sender could make a call to function withdraw() through its fallback function, before line 2 is executed. As a result, line 1 is executed again and another 20 wei is sent to the message sender. Eventually, all Ether in the wallet of this contract will be sent to the message sender.

In sCompile, inspired by common practice in banking industry, users are allowed to set a limit on the amount transferred out of the wallet of the contract. Assume that the user sets the limit to be 30. Given the contract, a critical program path reported by sCompile is one which executes line 0, 1, 0, and 1. The program path is associated with a warning message stating that the accumulated amount transferred along the path is more than the limit. With this information, it is easy to capture the vulnerability.

Example 3

contract Bitway is ERC20 {
       function () public payable {
              createTokens();
       }

       function createTokens() public payable {
              require(msg.value > 300);
              …
       }
       …
}

Contract Bitway is another token management contract. It receives Ether (i.e., cryptocurrency in Ethereum) through function createTokens(). Note that this is possible because function createTokens() is declared as payable. However, there is no function in the contract which can send Ether out. Given this contract, sCompile identifies a list of critical program paths for user inspection. The most critical one is a program path where function createTokens() is invoked. Furthermore, it is labeled with a warning message stating that the smart contract appears to be a “black hole” contract as there is no program path for sending Ether out, whereas this program path allows one to transfer Ether into the wallet of the contract. By inspecting this program path and the warning message, it is easy to capture the vulnerability.

Reference
“sCompile: Critical Path Identification and Analysis for Smart Contracts”, Jialiang Chang, Bo Gao, Hao Xiao, Jun Sun, Zijiang Yang, https://arxiv.org/abs/1808.00624