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

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

Permalink

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

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

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

Language

en

Permalink

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

Owning Collections