KEVM: A Complete Semantics of the Ethereum Virtual Machine

Hildenbrandt, Everett and Saxena, Manasvi and Zhu, Xiaoran and Rodrigues, Nishant and Daian, Philip and Guth, Dwight and Grigore Rosu, Grigore (2017) KEVM: A Complete Semantics of the Ethereum Virtual Machine. In: 2018 IEEE 31st Computer Security Foundations Symposium (CSF).

[img] Text
hildenbrandt-semantics-ethereum-virtual-machine.pdf
Restricted to Registered users only
Download (425kB)

Abstract

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.

Item Type: Conference or Workshop Item (Paper)
Subjects: Main Topics > Blockchain
Projects > BloSSom 2019
Main Topics > Distributed Systems
Main Topics > Ethereum
Main Topics > Security
Main Topics > Smart Contracts
Divisions: Computer Science
Depositing User: Unnamed user with email richard.dabels@uni-rostock.de
Date Deposited: 03 Sep 2019 16:33
Last Modified: 03 Sep 2019 16:33
URI: http://blossom.informatik.uni-rostock.de/id/eprint/16

Actions (login required)

View Item View Item
Blockchain is powered by EPrints 3 which is developed by the School of Electronics and Computer Science at the University of Southampton. More information and software credits.