Ethainter: A Smart Contract Security Analyzer for Composite Vulnerabilities
Lexi Brent∗
Int’l Computer Science Institute Berkeley, CA, USA
lexi@icsi.berkeley.edu
Neville Grech
University of Athens Athens, Greece
me@nevillegrech.com
Sifis Lagouvardos
University of Athens Athens, Greece
sifis.lag@di.uoa.gr
Bernhard Scholz
University of Sydney Sydney, NSW, Australia
bernhard.scholz@sydney.edu.au
Yannis Smaragdakis
University of Athens Athens, Greece
yannis@smaragd.org
Abstract
Smart contracts on permission less blockchains are exposed to inherent security risks due to interactions with untrusted entities. Static analyzers are essential for identifying security risks and avoiding millions of dollars worth of damage. We introduce Ethainter, a security analyzer checking information flow with data sanitization in smart contracts. Ethainter identifies composite attacks that involve an escalation of tainted information, through multiple transactions, leading to severe violations. The analysis scales to the entire blockchain, consisting of hundreds of thousands of unique smart contracts, deployed over millions of accounts. Ethainter is more precise than previous approaches, as we confirm by automatic exploit generation (e.g., destroying over 800 contracts on the Ropsten network) and by manual inspection, showing a very high precision of 82.5% valid warnings for end-to- nd vulnerabilities. Ethainter’s balance of precision and completeness offers significant advantages over other tools such as Securify, Securify2, and teEther.
CCS Concepts: · Software and its engineering → Formal software verification; · Theory of computation →Program analysis.
Keywords: static analysis, information flow, smart contracts
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from permissions@acm.org. PLDI ’20, June 15ś20, 2020, London, UK © 2020 Copyright held by the owner/author(s). Publication rights licensed to ACM. ACM ISBN 978-1-4503-7613-6/20/06. . . $15.
ACM Reference Format:
Lexi Brent, Neville Grech, Sifis Lagouvardos, Bernhard Scholz, and Yannis Smaragdakis. 2020. Ethainter: A Smart Contract Security Analyzer for Composite Vulnerabilities. In Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI ’20), June 15ś20, 2020, London, UK. ACM, New York
Introduction
Permissionless blockchain platforms such as Bitcoin [30] and Ethereum [6, 42] promise to revolutionize all sectors of multiparty interaction, by enabling decentralized, resilient consensus. The Ethereum platform, in particular, allows the execution of arbitrary programs, which are called smart contracts. Smart contracts are registered immutably on the blockchain and operate autonomously. Software correctness in smart contracts is critical, as (1) the contracts are high-value targets (since they manage monetary assets), (2) are immutable and cannot be patched, and (3) are fully available for inspection (and invocation) by potential attackers. The need for contract correctness has gained prominence via several recent high profile incidents resulting in losses of cryptocurrency amounts valued in the hundreds of millions [9, 41]. Smart contracts are Turing-complete programs, typically expressed in a domain-specific language called Solidity [40]. Solidity contracts are compiled to low-level bytecode and executed by the Ethereum Virtual Machine (EVM) on the blockchain. Smart contracts store data either on the blockchain or in execution-ephemeral memory. Solidity programs implement unconventional data structures using cryptographic hashing, posing a challenge for static bytecode analyzers. Furthermore, EVM bytecode does not explicitly expose control flow, necessitating sophisticated decomplication methodologies [5, 13, 24, 44]. Hence, checking for even basic security vulnerabilities is non-trivial, as security analyzers for smart contracts require complex techniques to overcome these challenges [14, 37].
With the rising awareness of Ethereum security risks and the development of recommended practices, realistic attacks have become increasingly complex. They often chain successive exploits that each expose more vulnerabilities. A new class of security analyzers is required to identify such composite attacks. The most notorious (albeit relatively simple) example of a composite attack is the Parity wallet hack, where the equivalent of $280M [9] was stolen or frozen via two separate vulnerabilities. The attack involved reinitializing part of the contract that sets owner variables, via a vulnerable library function, prior to attacking the contract.
To safeguard against sophisticated attacks, it is essential to model the information flow [34] inside smart contracts accurately. Information flow classifies information into trusted and untrusted and considers how it propagates in the code. For example, if untrusted (łtaintedž) information from external sources is allowed to spread to critical program points, it can alter key aspects of program behavior.
Smart contract programmers employ guarding patterns to prevent an untrusted entity from executing sensitive operations, such as destroying the contract. For example, the contract code could check whether the user of the contract (a.k.a., its caller or sender) has specific privileges. The simplest check is to permit only a particular contract owner account to perform critical actions. For security analyzers, it is essential to model this guarding mechanism, for any highfidelity information flow analysis: if guards are not taken into consideration, many contracts will be incorrectly inferred to be vulnerable, when the only user that can łexploitž these vulnerabilities would be the owner of the contract themselves. Conversely, the guarding code can itself be attacked, by invoking code that manipulates the state of the contract in unexpected ways.
In this work, we present Ethainter: the first security analyzer for detecting composite information flow violations in Ethereum smart contracts. Ethainter enhances the understanding of tainted information flow with the tainting of guard conditions, other potential ineffectiveness of guards, as well as different kinds of taint that are not prevented by guarding. Ethainter models not just the existence of guards but also whether they are effective in sanitizing information. The specification of the analysis is in a formalism of independent value. It ignores orthogonal, well-understood technical complexities, capturing, instead, the essence of new information flow concepts (e.g., tainted guards, taint through storage) in minimal form. For example, we consider a tainted memory store to induce further information flow more eagerly than an untainted (yet still statically undetermined) memory store. The precision, recall, and scalability of Ethainter are highly fine-tuned using mutually-recursive Datalog rules for tainting and overall information flow. The contribution of our work is as follows:
