A Semantic Framework for the Security Analysis of Ethereum smart contracts

By Ilya Grishchenko, Matteo Maffei, Clara Schneidewind. The post, 2018

309 citations recorded by the source corpus.

Smart contracts are programs running on cryptocurrency (e.g., Ethereum) blockchains, whose popularity stem from the possibility to perform financial transactions, such as payments and auctions, in a distributed environment without need for any trusted third party. Given their financial nature, bugs or vulnerabilities in these programs may lead to catastrophic consequences, as witnessed by recent attacks. Unfortunately, programming smart contracts is a delicate task that requires strong expertise: Ethereum smart contracts are written in Solidity, a dedicated language resembling JavaScript, and shipped over the blockchain in the EVM bytecode format. In order to rigorously verify the security of smart contracts, it is of paramount importance to formalize their semantics as well as the security properties of interest, in particular at the level of the bytecode being executed. In this paper, we present the first complete small-step semantics of EVM bytecode, which we formalize in the F* proof assistant, obtaining executable code that we successfully validate against the official Ethereum test suite. Furthermore, we formally define for the first time a number of central security properties for smart contracts, such as call integrity, atomicity, and independence from miner controlled parameters. This formalization relies on a combination of hyper- and safety properties. Along this work, we identified various mistakes and imprecisions in existing semantics and verification tools for Ethereum smart contracts, thereby demonstrating once more the importance of rigorous semantic foundations for the design of security verification techniques.

Subfields: Artificial Intelligence, Computer Networks and Communications, Information Systems

View Paper: https://www.semanticscholar.org/paper/3fefa6858fcc41d300b473249210ef165b113198

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computer Networks and Communications

In Information Systems

Citations in the corpus

Smart Contract Development: Challenges and Opportunities (2021, background): “has formalized a complete small-step semantics of EVM bytecode for the F* proof assistant [52].”
Using Blockchain for Electronic Health Records (2019, methodology): “That code is deployed and executed using the Ethereum Virtual Machine (EVM) [29], [31].”
Combining Graph Neural Networks With Expert Knowledge for Smart Contract Vulnerability Detection (2021, methodology): “ther, [23] and [24] define formal semantics of the EVM using the F* framework and the K framework, respectively.”
A Survey on Ethereum Systems Security (2019, background): “[146] (27) define a complete smallstep semantics of EVM bytecode and formalize most of the semantics in the proof assistant F* [147].”
Securify: Practical Security Analysis of Smart Contracts (2018, methodology): “While useful in some settings, these approaches come with several drawbacks: (i) they can miss critical violations (due to under-approximation), (ii) yet, can also produce false positives (due to imprecise modeling of domain-specific elements [33]), and (iii) they can fail to achieve sufficient code”
MadMax: surviving out-of-gas conditions in Ethereum smart contracts (2018, methodology): “Recently a complete small-step semantics of EVM bytecode has been formalized for the F* proof assistant [Grishchenko et al. 2018].”
Vandal: A Scalable Security Analysis Framework for Smart Contracts (2018, background): “Semi-automated formal veriﬁcation approaches have also been proposed [41– 46] for performing complete analyses of smart contracts using interactive theorem provers such as Isabelle/HOL [47], F* [48], Why3 [45], and K [49].”
Osiris: Hunting for Integer Bugs in Ethereum Smart Contracts (2018, background): “These mainly include attempts on formal verification [1, 2, 12, 15, 16, 30] and symbolic execution [18, 20, 23, 25, 26, 33].”
Survey on blockchain based smart contracts: Applications, opportunities and challenges (2021, methodology): “Grishchenko et al.[278] presented a complete smallstep semantics of EVM bytecode and formalized a significantly large fragment of EVM using F*, which is a popular programming language used for similar verification programmed proof assistant.”
Sereum: Protecting Existing Smart Contracts Against Re-Entrancy Attacks (2018, background): “Apart from the 6 false positives in our test set, the analysis performed by previous work [20], [42] demonstrated that re-entrancy detection in Oyente suffers from false positive issues.”
Finding The Greedy, Prodigal, and Suicidal Contracts at Scale (2018, methodology): “Various versions of EVM semantics [42] were implemented in Coq [23], Isabelle/HOL [3, 22], F⋆ [6, 18], Idris [34], and Why3 [14, 36], followed by subsequent mechanised contract verification efforts.”