Files in this item



application/pdfpark-zhang-rosu-2020-tr.pdf (762kB)
(no description provided)PDF


Title:End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract
Author(s):Park, Daejun; Zhang, Yi; Roşu, Grigore
Subject(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.
Issue Date:2020
Genre:Technical Report
Date Available in IDEALS:2020-05-14

This item appears in the following Collection(s)

Item Statistics