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 |