Zeus: Analyzing safety of smart contracts Kalra et al., NDSS’18

I’m sure many readers of The Morning Paper are also relatively experienced programmers. So how does this challenge sound? I want you to write a program that has to run in a concurrent environment under Byzantine circumstances where any adversary can invoke your program with any arguments of their choosing. The environment in which your program executes (and hence any direct or indirect environmental dependencies) is also under adversary control. If you make a single exploitable mistake or oversight in the implementation, or even in the logical design of the program, then either you personally or perhaps the users of your program could lose a substantial amount of money. Where your program will run, there is no legal recourse if things go wrong. Oh, and once you release the first version of your program, you can never change it. It has be right first time.

I don’t think there are many experienced programmers that would fancy taking on this challenge. But call it ‘writing a smart contract’ and programmers are lining up around the block to have a go! Most of them it seems, get it wrong.

Zeus is a framework for verifying the correctness and fairness of smart contracts:

We have built a prototype of Zeus for Ethereum and Fabric blockchain platforms, and evaluated it with over 22.4K smart contracts. Our evaluation indicates that about 94.6% of contracts (containing cryptocurrency worth more than $0.5B) are vulnerable…. (however, we do not investigate the practical exploitability of these bugs).

What could possibly go wrong?

We’ve studied some of the issues involved in writing smart contracts before. The authors of Zeus also provide a short summary of some of the ways that smart contracts can be incorrect or unfair. Implementation challenges leading to incorrect behaviour include:

• Reentrancy: multiple parallel external invocations are possible using the call family of constructs. If global state is not correctly managed, a contract can be vulnerable to reentrancy attacks. The related cross-function race condition can occur when two different functions operate on the same global state.

• Unchecked sends: upon a send call, a computation-heavy fallback function at the receiving contract can exhaust the available gas and cause the invoking send to fail. If this is not correctly handled it can lead to loss of Ether.

• Failed sends: best practices suggest executing a throw upon a failed send in order to revert the transaction. But this practice also has its risks. For example, in the following extract the throw causes loss of money to the DAO:

• Integer over or underflow: there are over 20 different scenarios that require careful handling of integer operations to avoid overflow or underflow. For example:

• Transaction state dependence: contract writers can utilise transaction state variables such as tx.origin for managing control flow within a contract. A crafty attacker can manipulate tx.origin (for example, using social engineering or phishing techniques) to their advantage.

Contracts may also end up being unfair due to logical design errors:

• Absence of required logic: for example, not guarding a call to selfdestruct with a check that only the owner of a contract is allowed to kill it.
• Incorrect logic: “there are many syntactically legal ways to achieve semantically unfair behaviour.” For example, the HackersGold contract had a bug where the transferFrom function used =+ in place of += and thus failed to increment a balance transferred to the recipient. (15 unique contracts in the data set had copies of the function with the same bug, and held over $ 35,000 worth of Ether between them).
• Logically correct but unfair designs. For example, an auction house contract that does not declare whether it is ‘with reserve,’ meaning that sellers can also bid or withdraw an item before it is sold. Unsuspecting bidders (with no expertise in examining the source code) could lose money due to artificially increased bids or forfeit their participation fee. (My personal view: when the code is the contract, and there is no other recourse, you’d really better be able to read the code if you want to participate). “This contract… indicates the subtleties involved in multi-party interactions, where fairness is subjective.”

Finally, miner’s also have some control over the environment in which contracts execute. Smart contract designers need to be aware of:

• Block state dependencies: many block state variables are determined from the block header, and thus vulnerable to tampering from the block miner.
• Transaction order dependencies: miners can reorder transactions and hence potentially influence their outcome.

A high-level description of Zeus

Of Zeus itself, we get only a relatively high-level description.

…Zeus takes as input a smart contract and a policy (written in a specification language) against which the smart contract must be verified. It performs static analysis atop the smart contract code and inserts policy predicates as assert statements at correct program points. Zeus then leverages its source code translator to faithfully convert the smart contract embedded with policy assertions to LLVM bitcode. Finally, Zeus invokes its verifier to determine assertion violations, which are indicative of policy violations.

Smart contracts are modelled using an abstract language that looks like this:

Programs are sequences of contract declarations, and each contract is viewed as a sequence of one or more method definitions in addition to the declaration and initialisation of persistent storage private to the contract. Contracts are identified by an Id, and the invocation of a publicly visible method on a contract is viewed as a transaction. Execution semantics are succinctly given in the following table:

(Enlarge).

A source code translator translates Solidity code into the abstract contract language.

The policy language enables a user to specify fairness rules for a contract. These rules are specified as XACML-styled five tuples with Subject, Object, Operation, Condition, and Result.

Our abstract language includes assertions for defining state reachability properties on the smart contract. Zeus leverages the policy tuple to extract: (a) predicate (i.e., Condition) to be asserted, and (b) the correct control location for inserting the assert statements in the program source.

Given the policy-enhanced program, Zeus translates it into LLVM bitcode. Here’s a simple end-to-end example showing the various components:

Finally, Zeus feeds the LLVM bitcode representation to an existing verification engine (Seahorn) that leverages constrained horn clauses (CHCs) to quickly ascertain the safety of the smart contract. Zeus is not tied to Seahorn though, in theory it could also be used with other verifiers operating on LLVM bitcode, such as SMACK or DIVINE.

Evaluating Solidity-based contracts

We periodically scraped Etherscan, Etherchain, and Ethercamp explorers over a period of three months and obtained source code for 22,493 contracts at distinct addresses. We discounted 45 contracts that had an assembly block in their source, and obtained 1524 unique contracts (as par their sha256 checksum). In the remainder of this section, we present results only for these unique contracts, unless otherwise specified.

The collected contracts divide up as follows:

Zeus checks for all of the correctness and miner’s influence issues are run across all of these contracts. Results are manually validated to determine the set of false positive and negatives. Zeus is also compared against the results from Oyente (‘Making smart contracts smarter’).

Here’s what Zeus finds:

(Enlarge).

• 21,281 out of 22,493 contracts (94.6%), containing more than $ 0.5 billion worth of Ether are vulnerable to one or more bugs. Across the unique contracts, 1194 out of 1524 contracts were found to be vulnerable to one or more bugs.
• There were zero false negatives across all seven of the bug classes.
• Verification is fast, with only 44 out of 1524 contracts (2.89%) timing out in at least one bug class. The timeout threshold was set at one minute.

To evaluate fairness the authors had to write some policies. As as example, for the CrowdFundDao the authors implemented policies that (a) blacklisted developers cannot participate in the scheme, and (b) an investment must be more than a threshold limit. Zeus is able to determine that neither of these checks are encoded in the contract. As a general purpose policy, the team wrote a policy that selfdestruct should only be called by the contract owner. 284 of the 1524 contracts included a selfdestruct, with 5.6% of them violating the policy.