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

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 high...

Descripción completa

Detalles Bibliográficos
Autores principales: Park, Daejun, Zhang, Yi, Rosu, Grigore
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7363177/
http://dx.doi.org/10.1007/978-3-030-53288-8_8
_version_ 1783559617712750592
author Park, Daejun
Zhang, Yi
Rosu, Grigore
author_facet Park, Daejun
Zhang, Yi
Rosu, Grigore
author_sort Park, Daejun
collection PubMed
description 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.
format Online
Article
Text
id pubmed-7363177
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-73631772020-07-16 End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract Park, Daejun Zhang, Yi Rosu, Grigore Computer Aided Verification Article 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. 2020-06-13 /pmc/articles/PMC7363177/ http://dx.doi.org/10.1007/978-3-030-53288-8_8 Text en © The Author(s) 2020 Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
spellingShingle Article
Park, Daejun
Zhang, Yi
Rosu, Grigore
End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract
title End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract
title_full End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract
title_fullStr End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract
title_full_unstemmed End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract
title_short End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract
title_sort end-to-end formal verification of ethereum 2.0 deposit smart contract
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7363177/
http://dx.doi.org/10.1007/978-3-030-53288-8_8
work_keys_str_mv AT parkdaejun endtoendformalverificationofethereum20depositsmartcontract
AT zhangyi endtoendformalverificationofethereum20depositsmartcontract
AT rosugrigore endtoendformalverificationofethereum20depositsmartcontract

Ejemplares similares