Research Summary - eThor: Practical and Provably Sound Static Analysis of Ethereum Smart Contracts

TLDR

  • The authors define and prove as sound a theoretical analysis of smart contract behavior that abstracts execution states and behavior using Horn clauses.
  • Security properties can be represented as reachability properties, making it possible to exclude unwanted states.
  • Using these principles, the team developed the eThor tool. Empirical evaluation confirms that eThor does not cause false negatives and outperforms the-state-of-the art analyzerits predecessor ZEUS.

Citation

  • “Schneidewind, C., Grishchenko, I., Scherer, M., & Maffei, M. (2020). eThor: Practical and Provably Sound Static Analysis of Ethereum Smart Contracts. CCS 2020“

Link

Core Research Question

  • How do you design an automated static analysis tool for Ethereum smart contracts that gives reliable guarantees for smart contract security?

Background

  • Ethereum smart contracts are distributed programs in the Ethereum cryptocurrency whose execution is part of consensus rules.
  • Ethereum smart contracts are entities in the Ethereum system that can own and control money and whose behavior is governed by their contract code. This characteristic is also described as the ‘Code-is-Law’-principle.
  • The native language of Ethereum smart contracts is Ethereum Virtual Machine (EVM) bytecode, an assembly-like bytecode format. Smart contracts are published on the blockchain in this format.
  • In practice, Ethereum smart contracts are written in high-level languages (typically Solidity) and then compiled to EVM bytecode.
  • Once a smart contract is created (which means a corresponding transaction that creates the contract is included in the blockchain), it is immutable. So buggy contracts cannot be patched once deployed.
  • The DAO hack illustrates this. This was an incident in 2016 where attackers exploited a smart contract-implemented venture capital fund called DAO (short for Decentralized Autonomous Organization). Attackers used a bug in the DAO contract’s code to steal funds worth more than $60M. According to the immutable nature of smart contracts and the ‘Code-is-Law’-principle, the buggy contract and the financial effects of the exploit should have been permanent. However, the community performed a hard fork to delete the DAO contract and revert the effects of the attack.
  • This led to a split of Ethereum into two currencies: Ethereum (which excludes the DAO hack) and Ethereum Classic (which follows the original consensus rules, including the DAO hack).

Abstract

  • Existing automated analysis tools for Ethereum smart contracts fail to give reliable guarantees. Tools that claim a positive analysis result would imply the security of a smart contract (with respect to a specific security property) can produce false negatives in practice, meaning they label contracts as secure when they violate the corresponding security property.
  • To solve this problem, the authors define a theoretical analysis that abstracts Ethereum smart contract execution states as logical predicates, and models an abstracted execution behavior as logical formulae (Horn clauses) over those predicates. The authors prove this abstraction to be sound,showing that if it is impossible to derive an abstract state using the logical formulas, then it is also impossible to reach any concrete execution state represented by this abstract state.
  • It is shown that relevant security properties for smart contracts can be represented as reachability properties, meaning they can be stated in terms of requiring certain problematic execution states to be unreachable. This in particular applies to a property called single-entrancy that rules out reentrancy vulnerabilities, such as the one enabling the DAO hack.
  • The eThor tool was implemented based on the previously presented theoretical analysis. To do so, the authors developed a new specification language (HoRSt) in which they formulate the theoretical analysis. This analysis specification is then automatically translated into input for the SMT-solver z3 which is used to solve the logical formulation of the analysis problem.
  • eThor was evaluated on the official Ethereum test suite as well as a set of real world contracts that was also used for the evaluation of the ZEUS[34] analyzer. Empirical evaluation confirms that eThor does not produce false negatives and that for the single-entrancy property it shows a better overall performance (considering precision and recall combined) than ZEUS.

Method

  • The paper combines theoretical modeling and logical proofs with an experimental evaluation of a tool that implements the described theory
  • Formal analysis specification: First the analysis technique is formally described. This is done by defining functions that translate concrete execution configurations of an Ethereum smart contract execution into abstract states. Next a (contract-dependent) set of logical formulas is defined that describes possible transitions between abstract states depending on the instructions in a contract.
  • Soundness proof: A logical soundness theorem is stated that characterizes the key property of the modeled analysis technique. The logical proof for this statement is conducted (in the appendix).
  • Empirical evaluation:
    • Testing: The analysis tool is run on the 604 relevant test cases of the official Ethereum test suite. It is shown that the analysis can always derive an abstract state that represents the test case result. Further it is shown that in 85% of the cases it can be verified that the test case can evaluate to nothing but the correct result.
    • Case Study: It is demonstrated on a real-world library contract (SafeMath) for safe mathematical operations, that the presented tool can prove functional properties, e.g., that the library functions cannot produce wrong results.
    • Large-scale experiment: The tool is evaluated for the single-entrancy property on a set of 605 unique real-world contracts from the Ethereum blockchain which was previously used for the analysis of the tool ZEUS. It shows a sensitivity of 100% and a specificity of 80%. These results are compared with the ZEUS tool that showed a sensitivity of 11% and a specificity of 99.8% on the same dataset for the single-entrancy property.

Results

  • The work presents the first automated static analyzer for Ethereum smart contracts that comes with provable soundness guarantees.

  • The presented analyzer shows a performance that is comparable to the one of existing analyzers which do not give guarantees on the analysis result.

  • The authors introduce the new specification language HoRSt that can be used to automatically generate analysis tools that are based on the same technique from logical analysis specifications.

Discussion & Key Takeaways

  • The authors trace the issues of other automated static analyzers back to subtleties in the semantics of Ethereum smart contracts, in particular to the fact that smart contracts do not behave like standard sequential programs.
  • As opposed to many other tools, eThor operates on the level of EVM bytecode, Ethereum’s low-level language. As a consequence its correctness cannot be corrupted by compiler bugs.
  • The authors note that the presented analysis tool targets smart contracts in a stand-alone setting. This implies that it is not possible to analyze the security of multiple known contracts (e.g., a contract together with the library contracts that it uses). As a consequence, contracts using specific instructions for accessing libraries do not fall into the scope of the analysis and are immediately considered unsafe. However, the authors argue that the analysis approach can be extended to account for such scenarios.
  • The authors discuss further potential refinements of the abstractions that they could incorporate in order to improve the precision of the analyzer (e.g., a more precise storage and memory representation)

Implications & Follow-ups

  • The presented tool allows users to derive provable guarantees on the execution behavior of Ethereum smart contracts. In contrast to heuristic tools that give an indication about security, a contract being labeled secure (with respect to some security property) by eThor inherits a security proof for this property.
  • A contract that is labelled insecure (with respect to a certain property) does not necessarily need to exhibit a vulnerability. In this case it was not possible for the tool to prove the contract’s security which can also be the result of imprecisions in the implemented analysis.
  • The authors discuss that in follow-ups of this work it would be interesting to improve the precision of the analyzer and to extend it to support more expressive security properties (e.g. dependency properties which can currently not be expressed)

Applicability

  • The work can be used for performing (semi-) automated security audits of Ethereum smart contracts.
    • On the one hand, the tool integrates some generic security properties (such as a check for single-entrancy). These checks can be automatically performed without further user interaction to ensure the absence of reentrancy vulnerabilities in the smart contract. Further, the tool allows to check automatically for the violation of assertions that are introduced on the level of the high-level language Solidity.
    • In the case study, it is demonstrated how the tool can be used to verify also (contract-specific) functional properties of a smart contract. This however requires that these functional properties are formulated on the level of bytecode.

[34] Sukrit Kalra, Seep Goel, Mohan Dhawan, and Subodh Sharma. 2018. ZEUS: Analyzing Safety of Smart Contracts. NDSS.

6 Likes