University of Illinois Urbana-Champaign

End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract

Park, Daejun; Zhang, Yi; Roşu, Grigore

Content Files
park-zhang-rosu-2020-tr.pdf

Permalink

https://hdl.handle.net/2142/107129

Description

Title
End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract
Author(s)
  • Park, Daejun
  • Zhang, Yi
  • Roşu, Grigore
Issue Date
2020
Keyword(s)
  • Formal Verification
  • Smart Contracts
Date of Ingest
2020-05-14T06:06:11Z
Abstract
We report our experience in the formal verification of the deposit smart contract, whose correctness is critical for the security of Ethereum 2.0, a new Proof-of-Stake protocol for the Ethereum blockchain. The deposit contract implements an incremental Merkle tree algorithm whose correctness is highly nontrivial, and had not been proved before. We have verified the correctness of the compiled bytecode of the deposit contract to avoid the need to trust the underlying compiler. We found several critical issues of the deposit contract during the verification process, some of which were due to subtle hidden bugs of the compiler.
Type of Resource
text
Genre of Resource
technical report
Language
en
Permalink
http://hdl.handle.net/2142/107129

Owning Collections

Research and Tech Reports - Computer Science PRIMARY