A formal verification tool for ethereum VM bytecode

Daejun Park, Yi Zhang, Manasvi Saxena, Philip Daian, Grigore Roşu

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 Kframework's reachability logic theorem prover to generate a correctby- 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.

Original languageEnglish (US)
Title of host publicationESEC/FSE 2018 - Proceedings of the 2018 26th ACM Joint Meeting on European So ftware Engineering Conference and Symposium on the Foundations of So ftware Engineering
EditorsAlessandro Garci, Corina S. Pasareanu, Gary T. Leavens
PublisherAssociation for Computing Machinery
Pages912-915
Number of pages4
ISBN (Electronic)9781450355735
DOIs
StatePublished - Oct 26 2018
Event26th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2018 - Lake Buena Vista, United States
Duration: Nov 4 2018Nov 9 2018

Publication series

NameESEC/FSE 2018 - Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering

Other

Other26th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2018
Country/TerritoryUnited States
CityLake Buena Vista
Period11/4/1811/9/18

Keywords

  • Ethereum
  • K framework
  • formal verification
  • smart contracts

ASJC Scopus subject areas

  • Software
  • Artificial Intelligence

Fingerprint

Dive into the research topics of 'A formal verification tool for ethereum VM bytecode'. Together they form a unique fingerprint.

Cite this