Document Open Access Logo

Formal Specification of the Cardano Blockchain Ledger, Mechanized in Agda

Authors Andre Knispel , Orestis Melkonian , James Chapman , Alasdair Hill, Joosep Jääger, William DeMeo , Ulf Norell

PDF
Thumbnail PDF

File

OASIcs.FMBC.2024.2.pdf
  • Filesize: 0.68 MB
  • 18 pages

Document Identifiers

Author Details

Andre Knispel
  • Input Output, Berlin, Germany
Orestis Melkonian
  • Input Output, Kirkwall, UK
James Chapman
  • Input Output, Glasgow, UK
Alasdair Hill
  • Input Output, Bristol, UK
Joosep Jääger
  • Input Output, Tartu, Estonia
William DeMeo
  • Input Output, Boulder, US
Ulf Norell
  • QuviQ, Göteborg, Sweden

Cite AsGet BibTex

Andre Knispel, Orestis Melkonian, James Chapman, Alasdair Hill, Joosep Jääger, William DeMeo, and Ulf Norell. Formal Specification of the Cardano Blockchain Ledger, Mechanized in Agda. In 5th International Workshop on Formal Methods for Blockchains (FMBC 2024). Open Access Series in Informatics (OASIcs), Volume 118, pp. 2:1-2:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/OASIcs.FMBC.2024.2

Abstract

Blockchain systems comprise critical software that handle substantial monetary funds, rendering them excellent candidates for formal verification. One of their core components is the underlying ledger that does all the accounting: keeping track of transactions and their validity, etc. Unfortunately, previous theoretical studies are typically confined to an idealized setting, while specifications for real implementations are scarce; either the functionality is directly implemented without a proper specification, or at best an informal specification is written on paper. The present work expands beyond prior meta-theoretical investigations of the EUTxO model to encompass the full scale of the Cardano blockchain: our formal specification describes a hierarchy of modular transitions that covers all the intricacies of a realistic blockchain, such as fully expressive smart contracts and decentralized governance. It is mechanized in a proof assistant, thus enjoys a higher standard of rigor: type-checking prevents minor oversights that were frequent in previous informal approaches; key meta-theoretical properties can now be formally proven; it is an executable specification against which the implementation in production is being tested for conformance; and it provides firm foundations for smart contract verification. Apart from a safety net to keep us in check, the formalization also provides a guideline for the ledger design: one informs the other in a symbiotic way, especially in the case of state-of-the-art features like decentralized governance, which is an emerging sub-field of blockchain research that however mandates a more exploratory approach. All the results presented in this paper have been mechanized in the Agda proof assistant and are publicly available. In fact, this document is itself a literate Agda script and all rendered code has been successfully type-checked.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Logic and verification
  • Theory of computation → Program specifications
Keywords
  • blockchain
  • distributed ledgers
  • UTxO
  • Cardano
  • formal verification
  • Agda

Metrics

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

Supplementary Materials

References

  1. Fahad F. Alhabardi, Arnold Beckmann, Bogdan Lazar, and Anton Setzer. Verification of Bitcoin Script in Agda using weakest preconditions for access control. In Henning Basold, Jesper Cockx, and Silvia Ghilezan, editors, 27th International Conference on Types for Proofs and Programs, TYPES 2021, June 14-18, 2021, Leiden, The Netherlands (Virtual Conference), volume 239 of LIPIcs, pages 1:1-1:25. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.TYPES.2021.1.
  2. Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, and Bas Spitters. Extracting smart contracts tested and verified in Coq. In Catalin Hritcu and Andrei Popescu, editors, CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021, pages 105-121. ACM, 2021. URL: https://doi.org/10.1145/3437992.3439934.
  3. Danil Annenkov, Jakob Botsch Nielsen, and Bas Spitters. Concert: a smart contract certification framework in Coq. In Jasmin Blanchette and Catalin Hritcu, editors, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, pages 215-228. ACM, 2020. URL: https://doi.org/10.1145/3372885.3373829.
  4. Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Jean-Christophe Filliatre, Eduardo Gimenez, Hugo Herbelin, Gerard Huet, Cesar Munoz, Chetan Murthy, et al. The Coq proof assistant reference manual: Version 6.1. PhD thesis, Inria, 1997. Google Scholar
  5. Bruno Bernardo, Raphaël Cauderlier, Guillaume Claret, Arvid Jakobsson, Basile Pesin, and Julien Tesson. Making tezos smart contracts more reliable with Coq. In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of Formal Methods, Verification and Validation: Applications - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part III, volume 12478 of Lecture Notes in Computer Science, pages 60-72. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-61467-6_5.
  6. Bruno Bernardo, Raphaël Cauderlier, Zhenlei Hu, Basile Pesin, and Julien Tesson. Mi-cho-coq, a framework for certifying Tezos smart contracts. In Emil Sekerinski, Nelma Moreira, José N. Oliveira, Daniel Ratiu, Riccardo Guidotti, Marie Farrell, Matt Luckcuck, Diego Marmsoler, José Creissac Campos, Troy Astarte, Laure Gonnord, Antonio Cerone, Luis Couto, Brijesh Dongol, Martin Kutrib, Pedro Monteiro, and David Delmas, editors, Formal Methods. FM 2019 International Workshops - Porto, Portugal, October 7-11, 2019, Revised Selected Papers, Part I, volume 12232 of Lecture Notes in Computer Science, pages 368-379. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-54994-7_28.
  7. Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Anitha Gollamudi, Georges Gonthier, Nadim Kobeissi, Natalia Kulatova, Aseem Rastogi, Thomas Sibut-Pinote, Nikhil Swamy, et al. Formal verification of smart contracts: Short paper. In Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security, pages 91-96, 2016. URL: https://doi.org/10.1145/2993600.2993611.
  8. Vitalik Buterin. A next-generation smart contract and decentralized application platform (white paper). https://ethereum.org/content/whitepaper/whitepaper-pdf/Ethereum_Whitepaper_-_Buterin_2014.pdf, 2014.
  9. Manuel M. T. Chakravarty, James Chapman, Kenneth MacKenzie, Orestis Melkonian, Michael Peyton Jones, and Philip Wadler. The Extended UTXO model. In Matthew Bernhard, Andrea Bracciali, L. Jean Camp, Shin'ichiro Matsuo, Alana Maurushat, Peter B. Rønne, and Massimiliano Sala, editors, Financial Cryptography and Data Security - FC 2020 International Workshops, AsiaUSEC, CoDeFi, VOTING, and WTSC, Kota Kinabalu, Malaysia, February 14, 2020, Revised Selected Papers, volume 12063 of Lecture Notes in Computer Science, pages 525-539. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-54455-3_37.
  10. Manuel M. T. Chakravarty, James Chapman, Kenneth MacKenzie, Orestis Melkonian, Jann Müller, Michael Peyton Jones, Polina Vinogradova, and Philip Wadler. Native custom tokens in the Extended UTXO model. In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of Formal Methods, Verification and Validation: Applications - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part III, volume 12478 of Lecture Notes in Computer Science, pages 89-111. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-61467-6_7.
  11. Xiaohong Chen, Daejun Park, and Grigore Roşu. A language-independent approach to smart contract verification. In International Symposium on Leveraging Applications of Formal Methods, pages 405-413. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-03427-6_30.
  12. Jared Corduan, Matthias Benkort, Kevin Hammond, Charles Hoskinson, Andre Knispel, and Samuel Leathers. A first step towards on-chain decentralized governance. https://cips.cardano.org/cip/CIP-1694, 2023.
  13. Bernardo Machado David, Peter Gazi, Aggelos Kiayias, and Alexander Russell. Ouroboros Praos: An adaptively-secure, semi-synchronous proof-of-stake protocol. IACR Cryptology ePrint Archive, 2017:573, 2017 . URL: http://eprint.iacr.org/2017/573.
  14. Christopher Goes. Compiling Quantitative Type Theory to Michelson for compile-time verification and run-time efficiency in juvix. In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of Formal Methods, Verification and Validation: Applications - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part III, volume 12478 of Lecture Notes in Computer Science, pages 146-160. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-61467-6_10.
  15. Neville Grech, Michael Kong, Anton Jurisevic, Lexi Brent, Bernhard Scholz, and Yannis Smaragdakis. Madmax: Surviving out-of-gas conditions in Ethereum smart contracts. Proceedings of the ACM on Programming Languages, 2(OOPSLA):1-27, 2018. URL: https://doi.org/10.1145/3276486.
  16. Andreas Haas, Andreas Rossberg, Derek L. Schuff, Ben L. Titzer, Michael Holman, Dan Gohman, Luke Wagner, Alon Zakai, and J. F. Bastien. Bringing the web up to speed with WebAssembly. In Albert Cohen and Martin T. Vechev, editors, Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, Barcelona, Spain, June 18-23, 2017, pages 185-200. ACM, 2017. URL: https://doi.org/10.1145/3062341.3062363.
  17. Philipp Kant, Kevin Hammond, Duncan Coutts, James Chapman, Nicholas Clarke, Jared Corduan, Neil Davies, Javier Díaz, Matthias Güdemann, Wolfgang Jeltsch, Marcin Szamotulski, and Polina Vinogradova. Flexible formality: Practical experience with agile formal methods. In Aleksander Byrski and John Hughes, editors, Trends in Functional Programming - 21st International Symposium, TFP 2020, Krakow, Poland, February 13-14, 2020, Revised Selected Papers, volume 12222 of Lecture Notes in Computer Science, pages 94-120. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-57761-2_5.
  18. Andre Knispel. Constructive zf-style set theory in type theory. unpublished, 2023. URL: https://whatisrt.github.io/papers/ZF-style-set-theory-in-type-theory.pdf.
  19. Andre Knispel, Orestis Melkonian, James Chapman, Alasdair Hill, Joosep Jääger, William DeMeo, and Ulf Norell. IntersectMBO/formal-ledger-specifications. swhId: https://archive.softwareheritage.org/swh:1:dir:085aefb014706c3ee4bcf1a9f85fcceaf10ba4cc;origin=https://github.com/IntersectMBO/formal-ledger-specifications;visit=swh:1:snp:5097bdc07a9030f7e251cb6529989d442bb82f35;anchor=swh:1:rev:002b7226a3af8e5e1068fd0c8fd1fcbb51bba64e, (visited on 06/05/2024). URL: https://github.com/IntersectMBO/formal-ledger-specifications.
  20. S. Nakamoto. Bitcoin: A peer-to-peer electronic cash system. https://bitcoin.org/en/bitcoin-paper, oct 2008.
  21. Eske Hoy Nielsen, Danil Annenkov, and Bas Spitters. Formalising decentralised exchanges in Coq. In Robbert Krebbers, Dmitriy Traytel, Brigitte Pientka, and Steve Zdancewic, editors, Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023, pages 290-302. ACM, 2023. URL: https://doi.org/10.1145/3573105.3575685.
  22. Jakob Botsch Nielsen and Bas Spitters. Smart contract interactions in Coq. In Emil Sekerinski, Nelma Moreira, José N. Oliveira, Daniel Ratiu, Riccardo Guidotti, Marie Farrell, Matt Luckcuck, Diego Marmsoler, José Creissac Campos, Troy Astarte, Laure Gonnord, Antonio Cerone, Luis Couto, Brijesh Dongol, Martin Kutrib, Pedro Monteiro, and David Delmas, editors, Formal Methods. FM 2019 International Workshops - Porto, Portugal, October 7-11, 2019, Revised Selected Papers, Part I, volume 12232 of Lecture Notes in Computer Science, pages 380-391. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-54994-7_29.
  23. Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel. Isabelle/HOL: a proof assistant for higher-order logic, volume 2283. Springer Science & Business Media, 2002. URL: https://doi.org/10.1007/3-540-45949-9.
  24. George Pîrlea and Ilya Sergey. Mechanising blockchain consensus. In June Andronick and Amy P. Felty, editors, Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, CA, USA, January 8-9, 2018, pages 78-90. ACM, 2018. URL: https://doi.org/10.1145/3167086.
  25. Ilya Sergey, Amrit Kumar, and Aquinas Hobor. Temporal properties of smart contracts. In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice - 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part IV, volume 11247 of Lecture Notes in Computer Science, pages 323-338. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-03427-6_25.
  26. Ilya Sergey, Vaivaswatha Nagaraj, Jacob Johannsen, Amrit Kumar, Anton Trunov, and Ken Chan Guan Hao. Safer smart contract programming with Scilla. Proc. ACM Program. Lang., 3(OOPSLA):185:1-185:30, 2019. URL: https://doi.org/10.1145/3360611.
  27. Anton Setzer. Modelling Bitcoin in Agda. CoRR, abs/1804.06398, 2018. URL: https://doi.org/10.48550/arXiv.1804.06398.
  28. Søren Eller Thomsen and Bas Spitters. Formalizing Nakamoto-style proof of stake. In 34th IEEE Computer Security Foundations Symposium, CSF 2021, Dubrovnik, Croatia, June 21-25, 2021, pages 1-15. IEEE, 2021. URL: https://doi.org/10.1109/CSF51468.2021.00042.
  29. Petar Tsankov. Security analysis of smart contracts in Datalog. In International Symposium on Leveraging Applications of Formal Methods, pages 316-322. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-03427-6_24.
  30. Conrad Watt. Mechanising and verifying the WebAssembly specification. In June Andronick and Amy P. Felty, editors, Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, CA, USA, January 8-9, 2018, pages 53-65. ACM, 2018. URL: https://doi.org/10.1145/3167082.
  31. Conrad Watt, Maja Trela, Peter Lammich, and Florian Märkl. Wasmref-isabelle: A verified monadic interpreter and industrial fuzzing oracle for WebAssembly. Proc. ACM Program. Lang., 7(PLDI):100-123, 2023. URL: https://doi.org/10.1145/3591224.
  32. Joachim Zahnentferner. Chimeric ledgers: Translating and unifying UTXO-based and account-based cryptocurrencies. Cryptology ePrint Archive, Report 2018/262, 2018. URL: https://eprint.iacr.org/2018/262.
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