KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine

By Everett Hildenbrandt, Manasvi Saxena, Nishant Rodrigues, Xiaoran Zhu, Philip Daian, Dwight Guth, Brandon M. Moore, D. Park, Yi Zhang, Andrei Stefanescu and 1 more. IEEE Computer Security Foundations Symposium, 2018

393 citations recorded by the source corpus.

A developing field of interest for the distributed systems and applied cryptography communities is that of smart contracts: self-executing financial instruments that synchronize their state, often through a blockchain. One such smart contract system that has seen widespread practical adoption is Ethereum, which has grown to a market capacity of 100 billion USD and clears an excess of 500,000 daily transactions. Unfortunately, the rise of these technologies has been marred by a series of costly bugs and exploits. Increasingly, the Ethereum community has turned to formal methods and rigorous program analysis tools. This trend holds great promise due to the relative simplicity of smart contracts and bounded-time deterministic execution inherent to the Ethereum Virtual Machine (EVM). Here we present KEVM, an executable formal specification of the EVM's bytecode stack-based language built with the K Framework, designed to serve as a solid foundation for further formal analyses. We empirically evaluate the correctness and performance of KEVM using the official Ethereum test suite. To demonstrate the usability, several extensions of the semantics are presented. and two different-language implementations of the ERC20 Standard Token are verified against the ERC20 specification. These results are encouraging for the executable semantics approach to language prototyping and specification.

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

View Paper: https://www.semanticscholar.org/paper/21bfb7d9014ffd758ec3be47fecb5e3cc1d26671

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

Blockchain-Enabled Smart Contracts: Architecture, Applications, and Future Trends (2019, methodology): “[56] presented KEVM, an executable formal specification of the EVM bytecode stack-based language built with the K Framework [57], which designed to serve as a solid foundation for further formal analyses.”
Securify: Practical Security Analysis of Smart Contracts (2018, methodology): “afety properties of smart contracts using existing interactive theorem provers. Formal semantics of the EVM have been defined by Grishchenko etal.[30] using the F* framework and by Hildenbrandt et al.[32] using the K framework [46]. These semantics are executable and were validated against the offic”
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.”
Empirical Review of Automated Analysis Tools on 47,587 Ethereum Smart Contracts (2019, neutral): “12 KEVM [21] https://github.”
A Survey on Ethereum Systems Security (2019, methodology): “[143] (25) present a complete semantics of the EVM, referred to as KEVM, using the K framework [144] to achieve language-independent program verification.”
Learning to Fuzz from Symbolic Execution with Application to Smart Contracts (2019, methodology): “KEVM [28] is an executable formal specification of EVM bytecode in the K Framework [50].”