eThor: Practical and Provably Sound Static Analysis of Ethereum Smart\n Contracts

Abstract

Ethereum has emerged as the most popular smart contract development platform,\nwith hundreds of thousands of contracts stored on the blockchain and covering a\nvariety of application scenarios, such as auctions, trading platforms, and so\non. Given their financial nature, security vulnerabilities may lead to\ncatastrophic consequences and, even worse, they can be hardly fixed as data\nstored on the blockchain, including the smart contract code itself, are\nimmutable. An automated security analysis of these contracts is thus of utmost\ninterest, but at the same time technically challenging for a variety of\nreasons, such as the specific transaction-oriented programming mechanisms,\nwhich feature a subtle semantics, and the fact that the blockchain data which\nthe contract under analysis interacts with, including the code of callers and\ncallees, are not statically known.\n In this work, we present eThor, the first sound and automated static analyzer\nfor EVM bytecode, which is based on an abstraction of the EVM bytecode\nsemantics based on Horn clauses. In particular, our static analysis supports\nreachability properties, which we show to be sufficient for capturing\ninteresting security properties for smart contracts (e.g., single-entrancy) as\nwell as contract-specific functional properties. Our analysis is proven sound\nagainst a complete semantics of EVM bytecode and an experimental large-scale\nevaluation on real-world contracts demonstrates that eThor is practical and\noutperforms the state-of-the-art static analyzers: specifically, eThor is the\nonly one to provide soundness guarantees, terminates on 95% of a representative\nset of real-world contracts, and achieves an F-measure (which combines\nsensitivity and specificity) of 89%.\n