A Formal Verification Tool for Ethereum VM Bytecode

From FSL
Revision as of 04:25, 3 August 2018 by Dpark69 (Talk | contribs)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

A Formal Verification Tool for Ethereum VM Bytecode
Daejun Park and Yi Zhang and Manasvi Saxena and Philip Daian and Grigore Rosu
ESEC/FSE'18, ACM, pp 912-915. 2018
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.
PDF, Slides(PDF), Formally Verified Smart Contracts, DOI, ESEC/FSE'18, BIB

Personal tools