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

Tooling and Languages
, , ,
1

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.

    1600×787 111 KB

  • 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.

    1374×600 72.1 KB

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.

9 Likes
2

Great summary! Can also include this link for testing this tool: Security & Privacy TU Wien

4 Likes
3

@tina1998612 that was a great suggestion, Tina – definitely nice to have a link to the software and a couple of presentations Clara and her team made. You’ve done hackathons and developed some blockchain products, how would you use something like eThor? Would it be enough security to develop a smart contract-based product for commercial use developer or are there other considerations you’d have?

2 Likes
4

Clara Schneidewind (@clara.schneidewind) was a Ph.D student at the Technical University of Vienna when the world’s first smart contract-enabled venture capital fund (The DAO) was hacked because of an unnoticed weakness in its low-level “bytecode.”

Schneidewind began looking at ways of mathematically proving whether an autonomously executed “smart contract” was secure, particularly at the level of programming where the Ethereum blockchain executes code.

eThor is a tool that her team developed from this research. It’s capable of testing whether a contract written in high-level Solidity (and other user-friendly high-level languages) remains secure when compiled into EVM bytecode.

  • Tools like eThor could be useful for creating plug-ins that would allow developers to test whether smart contracts are secure.
  • An eThor-like tool could also be used by auditors some day.
  • This tool could postpone the need for a programming language that has built-in security, which is one of the concerns about the Ethereum Virtual Machine.

We had a couple of questions for her about eThor and how it might work in the wild:

  • What would happen if a tool like this ended up in the hands of a nefarious actor? Could it be used to probe vulnerable smart contracts? What are the security implications of a tool like this?

  • What’s the update gap? How quickly could the protocol be updated if an exploit occurs?

  • How might something like eThor work at scale? How computationally complex is the tool? Is this a targeted deployment or something broader?

  • You mention that smart contracts are immutable, but there are design patterns that can be upgraded to fix bugs - how would eThor work around an upgrade?

  • What other security tools did you compare eThor with? How are eThor guarantees different than the ones with a tool like ZBM, for example?

  • How does eThor deal with contract initialization? What about delegate calls? If eThor works with libraries would it be possible to have an incorrectly stated negative?

  • What happens with smart contracts that contain loops?

2 Likes
5

Thank you a lot for the questions! I answered them below, but please let me know if anything is unclear and feel free to ask any follow-up questions!

What would happen if a tool like this ended up in the hands of a nefarious actor? Could it be used to probe vulnerable smart contracts? What are the security implications of a tool like this?

Generally, a tool like eThor that allows for automatic verification of smart contracts can always be used to scan the blockchain for potentially vulnerable smart contracts. However, eThor is not an attack generation tool. eThor can prove that a contract does not violate a certain security guarantee, but in case that it fails to prove, this does not imply that there is an attack. Also, it is (currently) very hard to reconstruct from the output of eThor a potential attack.

So, it requires substantial expertise by a nefarious actor to mount an attack on a contract flagged as potentially unsafe.
Still, of course, eThor can be used to narrow down the search space.

What’s the update gap? How quickly could the protocol be updated if an exploit occurs?

eThor is built in a very modular fashion. Actually, we developed a new specification language (HoRSt) that allows for giving the analysis specification in a human-readable format, and from this, the tool is automatically generated. This means that if there is the need for an update in the semantics of Ethereum byte code (e.g., since there was a bug discovered that affects the semantics), it is very fast to update eThor, since one only needs to adapt the specification.

How might something like eThor work at scale? How computationally complex is the tool? Is this a targeted deployment or something broader?

The general goal is that eThor should work at scale. Internally, the tool works by translation to an input format for SMT (Satisfiability Modulo Theories) solvers.

These solvers (e.g., z3) are highly optimized and very good at solving certain problem instances. Still, sometimes solving can take very long, or the solvers may even diverge on a contract. We optimized eThor for performance and evaluated its performance on real-world smart contracts. In our empirical evaluation, we ran eThor on 720 contracts from the blockchain, and within a 10-minute timeout (for each call in a contract), we could get results for 95% of them. This shows that eThor is suitable for the large-scale analysis of several contracts. However, the underlying SMT-solver is quite computationally heavy: Our experiments were performed on a server with 24 Cores at 2.8 GHz and 150 GiB of RAM. So for using eThor on a private laptop, one would need to calculate some more time. We still think that investing several minutes to check a contract for its safety is an overhead that might be acceptable for smart contract developers.

You mention that smart contracts are immutable, but there are design patterns that can be upgraded to fix bugs - how would eThor work around an upgrade?

eThor would not “work around” an upgrade but would just faithfully model the semantics of such an update mechanism.
For this reason, the answer to this question heavily depends on how eThor is used to analyze such a contract.

For the case of generic properties (e.g. single-entrancy as it is encoded at the moment), nothing about the current state of the contract is assumed.
For the described case, this would mean that eThor would over-approximate the behavior by assuming a behavior that subsumes all possible updates to the contract.
So, if some version of the contract (e.g., the initial one) would be buggy, eThor would classify the whole contract as such.

Still, eThor also supports more fine-grained reasoning, e.g., for user-defined functional properties. In this mode, the user could explicitly model the contract state after the upgrade and show that the contract is safe assuming this state.
However, since eThor works on low-level bytecode, the modeling of the state for a complex contract may be rather cumbersome.

What other security tools did you compare eThor with? How are eThor guarantees different than the ones with a tool like ZBM, for example?

In our work, we compared the performance of eThor to the tool ZEUS[1]. We chose that tool since it claims to come with soundness guarantees and since it conducted a large-scale analysis on a property similar to the single-entrancy one, which allowed for comparison.

We also looked into other tools claiming soundness (Securify[2], NeuCheck[3]) and could find counter-examples that challenge the soundness claims (also to the ones of ZEUS).
And this is also the crucial feature that differentiates eThor from other tools: It is proven that the theory underlying eThor (namely the core analysis and the encoding of the properties) faithfully abstracts (the formally defined) behavior of smart contract execution. This allows eThor to give a provable guarantee that security shown based on the analysis carries over to the real contract behavior. Other tools purely on rely on heuristics to detect potentially problematic behavior. This, in particular, means that if such a tool fails to find a bug, this does not guarantee the security of the contract.

How does eThor deal with contract initialization? What about delegate calls? If eThor works with libraries would it be possible to have an incorrectly stated negative?

The analyzer usually operates on the execution code (not the initialization code) of the contract.

In the standard case (e.g., for the analysis of single-entrancy), no assumption about the initial state of the contract is made (so it is assumed that any state could be possible). This can cause a loss in precision (but not in soundness) since modifications done during the initialization are not considered.

As described above, however, it is possible to use the ‘functional correctness mode’ of eThor to make assumptions about the state of the contract.
One could, e.g., prove that a certain invariant on the contract state is established by the initialization and then that this invariant is maintained in every execution. In that case, one could safely assume this invariant for further analysis.

For the case of delegate call, we currently assume every contract using it as potentially unsafe. This is a conservative choice to ensure soundness (absence of false negatives). When considering only a single contract, this choice is necessary since using delegate call may result in arbitrary states of the contract (when not assuming anything on the called library). So it cannot be excluded that these contract states violate the security property that is checked.

Since libraries, however, are an interesting use case and usually known upfront, we are currently working on the support for the compound verification of several known contracts. So that one could verify a contract together with the library and in this way get meaningful results.

What happens with smart contracts that contain loops?

Because eThor ultimately relies on SMT solvers, it can leverage their support for handling loops.
More precisely, we make use of the fixed point engines of these solvers.
These engines incorporate efficient heuristics to allow for (soundly) inferring loop invariants.
These heuristics are not always successful, but in this way, we can leverage the improvements of SMT solvers in this domain.

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

[2] Petar Tsankov, Andrei Dan, Dana Drachsler-Cohen, Arthur Gervais, Florian Bünzli, and Martin Vechev. 2018. Securify: Practical Security Analysis of Smart Contracts. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security (Toronto, Canada) (CCS). ACM, 67–82.

[3] Ning Lu, Bin Wang, Yongxin Zhang, Wenbo Shi, and Christian Esposito. 2019. NeuCheck: A more practical Ethereum smart contract security analysis tool. Software: Practice and Experience (2019).

https://onlinelibrary.wiley.com/doi/pdf/10.1002/spe.2745?casa_token=FNJPpeb7SUMAAAAA:553c1gxG2sNVdqW-pRnjthtvVu7u_QlqKREElnEbVce50VP7tQ9d6BBQ75jKwODe1iATo4IWGtqMEUWi

7 Likes