Skip to main content
Conference ProceedingsOPEN ACCESS

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

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (2020) 12224 LNCS 151-164
DOI: 10.1007/978-3-030-53288-8_8
20Citations
Citations of this article
23Readers
Mendeley users who have this article in their library.

This article is free to access.

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.

Cite

CITATION STYLE

APA

Park, D., Zhang, Y., & Rosu, G. (2020). End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 12224 LNCS, pp. 151–164). Springer. https://doi.org/10.1007/978-3-030-53288-8_8

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free