Trustworthy Systems

Towards verifying Ethereum smart contract bytecode in Isabelle/HOL

Authors

Sidney Amani, Myriam Begel, Maksym Bortin and Mark Staples

DATA61

UNSW Sydney

Abstract

Blockchain technology has increasing attention in research and across many industries. The Ethereum blockchain offers smart contracts, which are small programs defined, executed, and recorded as transactions in the blockchain transaction history. These smart contracts run on the Ethereum virtual machine (EVM) and can be used to encode agreements, transfer assets, and enforce integrity conditions in relationships between parties. Smart contracts can carry financial value, and are increasingly used for safety-, security-, or missioncritical purposes. Errors in smart contracts have and will lead to loss or harm. Formal verification can provide the highest level of confidence about the correct behaviour of smart contracts. In this paper we extend an existing EVM formalisation in Isabelle/HOL by a sound program logic at the level of bytecode. We structure bytecode sequences into basic blocks of straight-line code and create a program logic to reason about these. This abstraction is a step towards control of the cost and complexity of formal verification of EVM smart contracts.

BibTeX Entry

  @inproceedings{Amani_BBS_18,
    address          = {Los Angeles},
    author           = {Amani, Sidney and Begel, Myriam and Bortin, Maksym and Staples, Mark},
    booktitle        = {International Conference on Certified Programs and Proofs},
    date             = {2018-1-8},
    doi              = {https://doi.org/10.1145/3167084},
    isbn             = {978-1-4503-55},
    month            = jan,
    pages            = {66-77},
    paperurl         = {https://trustworthy.systems/publications/full_text/Amani_BBS_18.pdf},
    publisher        = {ACM},
    title            = {Towards Verifying {Ethereum} Smart Contract Bytecode in {Isabelle}/{HOL}},
    year             = {2018}
  }

Download