{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,6]],"date-time":"2026-03-06T18:35:52Z","timestamp":1772822152494,"version":"3.50.1"},"publisher-location":"Cham","reference-count":60,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030532871","type":"print"},{"value":"9783030532888","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,7,14]],"date-time":"2020-07-14T00:00:00Z","timestamp":1594684800000},"content-version":"vor","delay-in-days":195,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-53288-8_8","type":"book-chapter","created":{"date-parts":[[2020,7,15]],"date-time":"2020-07-15T19:03:27Z","timestamp":1594839807000},"page":"151-164","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":27,"title":["End-to-End Formal Verification of\u00a0Ethereum 2.0 Deposit Smart Contract"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1551-2597","authenticated-orcid":false,"given":"Daejun","family":"Park","sequence":"first","affiliation":[]},{"given":"Yi","family":"Zhang","sequence":"additional","affiliation":[]},{"given":"Grigore","family":"Rosu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,7,14]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Amani, S., B\u00e9gel, M., Bortin, M., Staples, M.: Towards verifying Ethereum smart contract bytecode in Isabelle\/hol. In: Proceedings of the 7th ACM International Conference on Certified Programs and Proofs, CPP 2018 (2018)","DOI":"10.1145\/3176245.3167084"},{"key":"8_CR2","unstructured":"Barnett, M., Chang, B.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: 4th International Symposium on Formal Methods for Components and Objects, FMCO 2005, Amsterdam, The Netherlands, November 1\u20134, 2005, Revised Lectures (2005)"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., et al.: Formal verification of smart contracts: Short paper. In: Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security, PLAS 2016 (2016)","DOI":"10.1145\/2993600.2993611"},{"key":"8_CR4","unstructured":"Bond, B., et al.: Vale: Verifying high-performance cryptographic assembly code. In: 26th USENIX Security Symposium, USENIX Security 2017, Vancouver, BC, Canada, August 16\u201318, 2017 (2017)"},{"key":"8_CR5","unstructured":"Brent, L., et al.: Vandal: a scalable security analysis framework for smart contracts. CoRR abs\/1809.03981 (2018)"},{"key":"8_CR6","unstructured":"Buterin, V.: Progressive Merkle Tree. \nhttps:\/\/github.com\/ethereum\/research\/blob\/master\/beacon_chain_impl\/progressive_merkle_tree.py"},{"key":"8_CR7","unstructured":"Buterin, V., Griffith, V.: Casper the friendly finality gadget. CoRR abs\/1710.09437 (2017)"},{"key":"8_CR8","unstructured":"Chen, H., Ziegler, D., Chajed, T., Chlipala, A., Kaashoek, M.F., Zeldovich, N.: Using crash hoare logic for certifying the FSCQ file system. In: Proceedings of the 25th Symposium on Operating Systems Principles, SOSP 2015, Monterey, CA, USA, October 4\u20137, 2015 (2015)"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/978-3-319-96142-2_26","volume-title":"Computer Aided Verification","author":"A Chudnov","year":"2018","unstructured":"Chudnov, A., et al.: Continuous formal verification of Amazon s2n. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 430\u2013446. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-96142-2_26"},{"key":"8_CR10","unstructured":"ConsenSys Diligence: MythX. \nhttps:\/\/mythx.io\/"},{"key":"8_CR11","unstructured":"ConsenSys Diligence: Vyper Security Review. \nhttps:\/\/diligence.consensys.net\/audits\/2019\/10\/vyper\/"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1007\/978-3-319-96142-2_28","volume-title":"Computer Aided Verification","author":"B Cook","year":"2018","unstructured":"Cook, B., Khazem, K., Kroening, D., Tasiran, S., Tautschnig, M., Tuttle, M.R.: Model checking boot code from AWS data centers. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 467\u2013486. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-96142-2_28"},{"key":"8_CR13","unstructured":"Ethereum Foundation: Contract ABI Specification. \nhttps:\/\/solidity.readthedocs.io\/en\/v0.6.1\/abi-spec.html"},{"key":"8_CR14","unstructured":"Ethereum Foundation: Ethereum 2.0 Deposit Contract. \nhttps:\/\/github.com\/ethereum\/eth2.0-specs\/blob\/v0.11.2\/deposit_contract\/contracts\/validator_registration.vy"},{"key":"8_CR15","unstructured":"Ethereum Foundation: Ethereum 2.0 Specifications. \nhttps:\/\/github.com\/ethereum\/eth2.0-specs"},{"key":"8_CR16","unstructured":"Ethereum Foundation: Ethereum Foundation Spring 2019 Update. \nhttps:\/\/blog.ethereum.org\/2019\/05\/21\/ethereum-foundation-spring-2019-update\/"},{"key":"8_CR17","unstructured":"Ethereum Foundation: Hardfork Meta: Istanbul. \nhttps:\/\/github.com\/ethereum\/EIPs\/blob\/master\/EIPS\/eip-1679.md"},{"key":"8_CR18","unstructured":"Ethereum Foundation: SimpleSerialize (SSZ). \nhttps:\/\/github.com\/ethereum\/eth2.0-specs\/tree\/dev\/ssz"},{"key":"8_CR19","unstructured":"Ethereum Foundation: Vyper. \nhttps:\/\/vyper.readthedocs.io"},{"key":"8_CR20","unstructured":"Feist, J., Grieco, G., Groce, A.: Slither: a static analysis framework for smart contracts. In: Proceedings of the 2nd International Workshop on Emerging Trends in Software Engineering for Blockchain, WETSEB@ICSE 2019, Montreal, QC, Canada, May 27, 2019 (2019)"},{"key":"8_CR21","unstructured":"Gnosis Ltd.: Gnosis Safe. \nhttps:\/\/safe.gnosis.io\/"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Grishchenko, I., Maffei, M., Schneidewind, C.: A semantic framework for the security analysis of Ethereum smart contracts. In: Proceedings of the 7th International Conference on Principles of Security and Trust, POST 2018 (2018)","DOI":"10.1007\/978-3-319-89722-6_10"},{"key":"8_CR23","unstructured":"Gu, R., et al.: Certikos: an extensible architecture for building certified concurrent OS kernels. In: 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016, Savannah, GA, USA, November 2\u20134, 2016 (2016)"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Hildenbrandt, E., et al.: Kevm: a complete semantics of the Ethereum virtual machine. In: Proceedings of the 31st IEEE Computer Security Foundations Symposium, CSF 2018 (2018)","DOI":"10.1109\/CSF.2018.00022"},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"Kalra, S., Goel, S., Dhawan, M., Sharma, S.: ZEUS: analyzing safety of smart contracts. In: Proceedings of the 25th Annual Network and Distributed System Security Symposium, NDSS 2018 (2018)","DOI":"10.14722\/ndss.2018.23082"},{"key":"8_CR26","unstructured":"Klein, G., et al.: sel4: formal verification of an OS kernel. In: Proceedings of the 22nd ACM Symposium on Operating Systems Principles 2009, SOSP 2009, Big Sky, Montana, USA, October 11\u201314, 2009 (2009)"},{"key":"8_CR27","unstructured":"Lahiri, S.K., Chen, S., Wang, Y., Dillig, I.: Formal specification and verification of smart contracts for azure blockchain. CoRR abs\/1812.08829 (2018)"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"Luu, L., Chu, D.H., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, CCS 2016 (2016)","DOI":"10.1145\/2976749.2978309"},{"key":"8_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/978-3-030-03427-6_33","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice","author":"M Marescotti","year":"2018","unstructured":"Marescotti, M., Blicha, M., Hyv\u00e4rinen, A.E.J., Asadi, S., Sharygina, N.: Computing exact worst-case gas consumption for smart contracts. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11247, pp. 450\u2013465. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-030-03427-6_33"},{"key":"8_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/3-540-48184-2_32","volume-title":"Advances in Cryptology \u2014 CRYPTO\u201987","author":"RC Merkle","year":"1988","unstructured":"Merkle, R.C.: A digital signature based on a conventional encryption function. In: Pomerance, C. (ed.) CRYPTO 1987. LNCS, vol. 293, pp. 369\u2013378. Springer, Heidelberg (1988). \nhttps:\/\/doi.org\/10.1007\/3-540-48184-2_32"},{"key":"8_CR31","unstructured":"Nelson, L., et al.: Hyperkernel: push-button verification of an OS kernel. In: Proceedings of the 26th Symposium on Operating Systems Principles, Shanghai, China, October 28\u201331, 2017 (2017)"},{"key":"8_CR32","unstructured":"Nikolic, I., Kolluri, A., Sergey, I., Saxena, P., Hobor, A.: Finding the greedy, prodigal, and suicidal contracts at scale. In: Proceedings of the 34th Annual Computer Security Applications Conference, ACSAC 2018, San Juan, PR, USA, December 03\u201307, 2018 (2018)"},{"key":"8_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL- A Proof Assistant for Higher-Order Logic","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL- A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). \nhttps:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"8_CR34","unstructured":"NIST: Perfect Binary Tree. \nhttps:\/\/xlinux.nist.gov\/dads\/HTML\/perfectBinaryTree.html"},{"key":"8_CR35","unstructured":"Park, D.: Ethereum 2.0 Deposit Contract Issue 1341: Non ABI-standard return value of get$$\\_$$deposit$$\\_$$count of deposit contract. \nhttps:\/\/github.com\/ethereum\/eth2.0-specs\/issues\/1341"},{"key":"8_CR36","unstructured":"Park, D.: Ethereum 2.0 Deposit Contract Issue 1357: Ill-formed call data to deposit contract can add invalid deposit data. \nhttps:\/\/github.com\/ethereum\/eth2.0-specs\/issues\/1357"},{"key":"8_CR37","unstructured":"Park, D.: Ethereum 2.0 Deposit Contract Issue 26: Maximum deposit count. \nhttps:\/\/github.com\/ethereum\/deposit_contract\/issues\/26"},{"key":"8_CR38","unstructured":"Park, D.: Ethereum 2.0 Deposit Contract Issue 27: Redundant assignment in init(). \nhttps:\/\/github.com\/ethereum\/deposit_contract\/issues\/27"},{"key":"8_CR39","unstructured":"Park, D.: Ethereum 2.0 Deposit Contract Issue 28: Loop fusion optimization. \nhttps:\/\/github.com\/ethereum\/deposit_contract\/issues\/28"},{"key":"8_CR40","unstructured":"Park, D.: Ethereum 2.0 Deposit Contract Issue 38: A refactoring suggestion for the loop of deposit(). \nhttps:\/\/github.com\/ethereum\/deposit_contract\/issues\/38"},{"key":"8_CR41","unstructured":"Park, D.: Vyper Issue 1563: Insufficient zero-padding bug for functions returning byte arrays of size $$<$$ 16. \nhttps:\/\/github.com\/vyperlang\/vyper\/issues\/1563"},{"key":"8_CR42","unstructured":"Park, D.: Vyper Issue 1599: Off-by-one error in zero$$\\_$$pad(). \nhttps:\/\/github.com\/vyperlang\/vyper\/issues\/1599"},{"key":"8_CR43","unstructured":"Park, D.: Vyper Issue 1610: Non-semantics-preserving refactoring for zero$$\\_$$pad(). \nhttps:\/\/github.com\/vyperlang\/vyper\/issues\/1610"},{"key":"8_CR44","unstructured":"Park, D.: Vyper Issue 1761: Potentially insufficient gas stipend for precompiled contract calls. \nhttps:\/\/github.com\/vyperlang\/vyper\/issues\/1761"},{"key":"8_CR45","unstructured":"Park, D., Zhang, Y., Rosu, G.: End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract. \nhttp:\/\/hdl.handle.net\/2142\/107129"},{"key":"8_CR46","doi-asserted-by":"crossref","unstructured":"Park, D., Zhang, Y., Saxena, M., Daian, P., Ro\u015fu, G.: A formal verification tool for Ethereum VM Bytecode. In: Proceedings of the 26th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC\/FSE 2018 (2018)","DOI":"10.1145\/3236024.3264591"},{"key":"8_CR47","unstructured":"Permenev, A., Dimitrov, D., Tsankov, P., Drachsler-Cohen, D., Vechev, M.: VerX: Safety Verification of Smart Contracts. \nhttps:\/\/files.sri.inf.ethz.ch\/website\/papers\/sp20-verx.pdf"},{"key":"8_CR48","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, LICS 2004 (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"key":"8_CR49","unstructured":"Runtime Verification Inc: Bytecode Behavior Specification of Ethereum 2.0 Deposit Contract. \nhttps:\/\/github.com\/runtimeverification\/verified-smart-contracts\/blob\/master\/deposit\/bytecode-verification\/deposit-spec.ini.md"},{"key":"8_CR50","unstructured":"Runtime Verification Inc.: Formal Verification of Ethereum 2.0 Deposit Contract. \nhttps:\/\/github.com\/runtimeverification\/verified-smart-contracts\/tree\/master\/deposit"},{"key":"8_CR51","unstructured":"Runtime Verification Inc.: Formally Verified Smart Contracts. \nhttps:\/\/github.com\/runtimeverification\/verified-smart-contracts"},{"key":"8_CR52","unstructured":"Serbanuta, T., Arusoaie, A., Lazar, D., Ellison, C., Lucanu, D., Rosu, G.: The K primer (version 3.3). Electr. Notes Theor. Comput. Sci. 304, 57\u201380 (2014)"},{"key":"8_CR53","unstructured":"Sigurbjarnarson, H., Bornholt, J., Torlak, E., Wang, X.: Push-button verification of file systems via crash refinement. In: 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016, Savannah, GA, USA, November 2\u20134, 2016 (2016)"},{"key":"8_CR54","unstructured":"Stefanescu, A., Ciobaca, S., Mereuta, R., Moore, B.M., Serbanuta, T., Rosu, G.: All-Path Reachability Logic. Logical Methods in Computer Science 15(2), (2019)"},{"key":"8_CR55","doi-asserted-by":"crossref","unstructured":"Stefanescu, A., Park, D., Yuwen, S., Li, Y., Rosu, G.: Semantics-based program verifiers for all languages. In: Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016 (2016)","DOI":"10.1145\/2983990.2984027"},{"key":"8_CR56","unstructured":"Swamy, N., et al.: Dependent types and multi-monadic effects in F. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20\u201322, 2016 (2016)"},{"key":"8_CR57","unstructured":"Tikhomirov, S., Voskresenskaya, E., Ivanitskiy, I., Takhaviev, R., Marchenko, E., Alexandrov, Y.: Smartcheck: Static analysis of Ethereum smart contracts. In: 1st IEEE\/ACM International Workshop on Emerging Trends in Software Engineering for Blockchain, WETSEB@ICSE 2018, Gothenburg, Sweden, May 27\u2013June 3, 2018 (2018)"},{"key":"8_CR58","unstructured":"Tsankov, P., Dan, A.M., Drachsler-Cohen, D., Gervais, A., B\u00fcnzli, F., Vechev, M.T.: Securify: practical security analysis of smart contracts. In: Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018, Toronto, ON, Canada, October 15\u201319, 2018 (2018)"},{"key":"8_CR59","unstructured":"Uniswap: Uniswap Exchange Protocol. \nhttps:\/\/uniswap.io\/"},{"key":"8_CR60","unstructured":"Wood, G.: Ethereum: A Secure Decentralised Generalised Transaction Ledger. \nhttps:\/\/ethereum.github.io\/yellowpaper\/paper.pdf"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-53288-8_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,15]],"date-time":"2020-07-15T19:06:41Z","timestamp":1594840001000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-53288-8_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030532871","9783030532888"],"references-count":60,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-53288-8_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"14 July 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Los Angeles, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair.org","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"240","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"43","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"22","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"18% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}