Journal
IEEE 31ST COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF 2018)
Volume -, Issue -, Pages 204-217Publisher
IEEE COMPUTER SOC
DOI: 10.1109/CSF.2018.00022
Keywords
-
Categories
Funding
- Boeing grant on Formal Analysis Tools for Cyber Security 2016-2017
- NSF [CCF-1318191, CCF-1421575, CNS-1330599, CNS-1514163, IIP-1660186, DGE-1650441]
- Ethereum Foundation
- IOHK
Ask authors/readers for more resources
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 In 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 14 the executable semantics approach to language prototyping and specification.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available