A Formal Verification Tool for Ethereum VM Bytecode
Title | A Formal Verification Tool for Ethereum VM Bytecode |
Publication Type | Conference Paper |
Year of Publication | 2018 |
Authors | Park, Daejun, Zhang, Yi, Saxena, Manasvi, Daian, Philip, Ro\c su, Grigore |
Conference Name | Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering |
Publisher | ACM |
ISBN Number | 978-1-4503-5573-5 |
Keywords | compositionality, ethereum, formal verification, K framework, Metrics, pubcrawl, resilience, Resiliency, Scalability, scalable verification, smart contracts |
Abstract | In this paper, we present a formal verification tool for the Ethereum Virtual Machine (EVM) bytecode. To precisely reason about all possible behaviors of the EVM bytecode, we adopted KEVM, a complete formal semantics of the EVM, and instantiated the K-framework's reachability logic theorem prover to generate a correct-by-construction deductive verifier for the EVM. We further optimized the verifier by introducing EVM-specific abstractions and lemmas to improve its scalability. Our EVM verifier has been used to verify various high-profile smart contracts including the ERC20 token, Ethereum Casper, and DappHub MakerDAO contracts. |
URL | https://dl.acm.org/citation.cfm?doid=3236024.3264591 |
DOI | 10.1145/3236024.3264591 |
Citation Key | park_formal_2018 |