A formal verification tool for Ethereum VM bytecode

Daejun Park, Yi Zhang, Manasvi Saxena, Philip Daian, Grigore Rosu

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.

BibTeX

@inproceedings{Park-al:FSE18,
  author    = {Daejun Park and
               Yi Zhang and
               Manasvi Saxena and
               Philip Daian and
               Grigore Rosu},
  title     = {A formal verification tool for Ethereum {VM} bytecode},
  booktitle = {{ESEC/SIGSOFT} {FSE}},
  pages     = {912--915},
  publisher = {{ACM}},
  year      = {2018},
}

A formal verification tool for Ethereum VM bytecode

Abstract

Related papers