Document Open Access Logo

Towards Formally Specifying and Verifying Smart Contract Upgrades in Coq

Author Derek Sorensen

PDF
Thumbnail PDF

File

OASIcs.FMBC.2024.7.pdf
  • Filesize: 0.57 MB
  • 14 pages

Document Identifiers

Author Details

Derek Sorensen
  • Department of Computer Science and Technology, University of Cambridge, UK

Cite AsGet BibTex

Derek Sorensen. Towards Formally Specifying and Verifying Smart Contract Upgrades in Coq. In 5th International Workshop on Formal Methods for Blockchains (FMBC 2024). Open Access Series in Informatics (OASIcs), Volume 118, pp. 7:1-7:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/OASIcs.FMBC.2024.7

Abstract

Smart contract upgrades are costly from a verification perspective and can be a meaningful source of vulnerabilities when done incorrectly. Unfortunately, there is no established, formal framework through which one can reason about contracts as they undergo upgrades, though much work has been done to verify standalone smart contracts. Instead, one must repeat the full verification process for each contract upgrade, something which relies heavily on fallible intuition, can lead to unexpected vulnerabilities, and drives up the cost of formally verifying smart contracts. We propose a formal framework for contract upgrades in ConCert, a Coq-based smart contract verification tool. Central to this framework is our notion of a contract morphism, a theoretical tool which we introduce to formally encode structural relationships between smart contracts, and with which we can formally specify and verify an upgraded contract relative to its previous versions. We argue that ours is a natural framework for specifying and verifying contract upgrades, and hope to offer a first step towards rigorous, efficient specification and verification of contract upgrades.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program verification
Keywords
  • smart contract verification
  • formal methods
  • interactive theorem prover
  • smart contract upgrades

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, and Bas Spitters. Extracting smart contracts tested and verified in Coq. In Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, pages 105-121, New York, NY, USA, jan 2021. Association for Computing Machinery. URL: https://doi.org/10.1145/3437992.3439934.
  2. Danil Annenkov, Jakob Botsch Nielsen, and Bas Spitters. ConCert: A smart contract certification framework in Coq. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pages 215-228, New York, NY, USA, jan 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3372885.3373829.
  3. Pedro Antonino, Juliandson Ferreira, Augusto Sampaio, and A. W. Roscoe. Specification is Law: Safe Creation and Upgrade of Ethereum Smart Contracts. In Software Engineering and Formal Methods: 20th International Conference, SEFM 2022, Berlin, Germany, September 26endash 30, 2022, Proceedings, pages 227-243. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-17108-6_14.
  4. Rob Behnke. Explained: The NowSwap Protocol Hack. https://halborn.com/explained-the-nowswap-protocol-hack-september-2021/, sep 2021. Accessed January 2024. Google Scholar
  5. Cyril Cohen, Maxime Dénès, and Anders Mörtberg. Refinements for free! In International Conference on Certified Programs and Proofs, pages 147-162. Springer, 2013. URL: https://doi.org/10.1007/978-3-319-03545-1_10.
  6. Thomas Dickerson, Paul Gazzillo, Maurice Herlihy, Vikram Saraph, and Eric Koskinen. Proof-Carrying Smart Contracts. In Aviv Zohar, Ittay Eyal, Vanessa Teague, Jeremy Clark, Andrea Bracciali, Federico Pintore, and Massimiliano Sala, editors, Financial Cryptography and Data Security, Lecture Notes in Computer Science, pages 325-338, Berlin, Heidelberg, 2019. Springer. URL: https://doi.org/10.1007/978-3-662-58820-8_22.
  7. etherscan.io. Nomad Bridge Exploit. Transaction 0xa5fe9d044e4f3e5aa5bc4c0709333cd2190cba0f4e7f16bcf73f49f83e4a5460, 2022. Google Scholar
  8. Uranium Finance. Uranium Finance Exploit. https://uraniumfinance.medium.com/exploit-d3a88921531c, apr 2021. Accessed January 2024. Google Scholar
  9. Immunefi. Hack Analysis: Nomad Bridge, August 2022. https://medium.com/immunefi/hack-analysis-nomad-bridge-august-2022-5aa63d53814a, jan 2023. Google Scholar
  10. Oussama Jebbar, Ferhat Khendek, and Maria Toeroe. Upgrade of highly available systems: Formal methods at the rescue. In 2017 IEEE International Conference on Information Reuse and Integration (IRI), pages 270-274. IEEE, 2017. URL: https://doi.org/10.1109/IRI.2017.66.
  11. Nicolas Magaud and Yves Bertot. Changing data structures in type theory: A study of natural numbers. In International Workshop on Types for Proofs and Programs, pages 181-196. Springer, 2000. URL: https://doi.org/10.1007/3-540-45842-5_12.
  12. Stephen McCamant and Michael D Ernst. Predicting problems caused by component upgrades. In Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering, pages 287-296, 2003. URL: https://doi.org/10.1145/940071.940110.
  13. Nick Mudge. EIP-2535: Diamonds, Multi-Facet Proxy. https://eips.ethereum.org/EIPS/eip-2535. Accessed January 2024.
  14. Talia Ringer. Proof Repair. University of Washington, 2021. URL: https://hdl.handle.net/1773/47429.
  15. Talia Ringer, RanDair Porter, Nathaniel Yazdani, John Leo, and Dan Grossman. Proof repair across type equivalences. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pages 112-127, 2021. URL: https://doi.org/10.1145/3453483.3454033.
  16. Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman. Adapting proof automation to adapt proofs. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 115-129, 2018. URL: https://doi.org/10.1145/3167094.
  17. Davide Sangiorgi. On the bisimulation proof method. Mathematical Structures in Computer Science, 8(5):447-479, oct 1998. URL: https://doi.org/10.1017/S0960129598002527.
  18. Amritraj Singh, Reza M Parizi, Qi Zhang, Kim-Kwang Raymond Choo, and Ali Dehghantanha. Blockchain smart contracts formalization: Approaches and challenges to address vulnerabilities. Computers & Security, 88:101654, 2020. URL: https://doi.org/10.1016/j.cose.2019.101654.
  19. Derek Sorensen. FinCert. swhId: https://archive.softwareheritage.org/swh:1:dir:a0d8499f935e75e7076b33b666898752e27cbf3d;origin=https://github.com/dhsorens/FinCert;visit=swh:1:snp:0cbe1a324310e49b943e1e64ae9a3df868a009a6;anchor=swh:1:rev:5fe1e6d94ac519890d1dac0d283b3969fc84bb1a, (visited on 02/05/2024). URL: https://github.com/dhsorens/FinCert.
  20. Derek Sorensen. (In)Correct Smart Contract Specifications. IEEE International Conference on Blockchain and Cryptocurrency (ICBC), 2024. Google Scholar
  21. Nicolas Tabareau, Éric Tanter, and Matthieu Sozeau. Equivalences for free: univalent parametricity for effective transport. Proceedings of the ACM on Programming Languages, 2(ICFP):1-29, 2018. URL: https://doi.org/10.1145/3236787.
  22. Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst, and Thomas Anderson. Planning for change in a formal verification of the raft consensus protocol. In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2016, pages 154-165, New York, NY, USA, 2016. Association for Computing Machinery. URL: https://doi.org/10.1145/2854065.2854081.
  23. Jiahua Xu, Krzysztof Paruch, Simon Cousaert, and Yebo Feng. SoK: Decentralized Exchanges (DEX) with Automated Market Maker (AMM) Protocols. ACM Computing Surveys, 55(11):1-50, 2023. URL: https://doi.org/10.1145/3570639.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact