Document Open Access Logo

Structured Contracts in the EUTxO Ledger Model

Authors Polina Vinogradova , Orestis Melkonian , Philip Wadler , Manuel Chakravarty, Jacco Krijnen , Michael Peyton Jones , James Chapman , Tudor Ferariu

PDF
Thumbnail PDF

File

OASIcs.FMBC.2024.10.pdf
  • Filesize: 0.82 MB
  • 19 pages

Document Identifiers

Author Details

Polina Vinogradova
  • Input Output, Canada
Orestis Melkonian
  • Input Output, United Kingdom
Philip Wadler
  • Input Output, United Kingdom
  • University of Edinburgh, United Kingdom
Manuel Chakravarty
  • Input Output, The Netherlands
Jacco Krijnen
  • Utrecht University, The Netherlands
Michael Peyton Jones
  • Input Output, United Kingdom
James Chapman
  • Input Output, United Kingdom
Tudor Ferariu
  • University of Edinburgh, United Kingdom

Cite AsGet BibTex

Polina Vinogradova, Orestis Melkonian, Philip Wadler, Manuel Chakravarty, Jacco Krijnen, Michael Peyton Jones, James Chapman, and Tudor Ferariu. Structured Contracts in the EUTxO Ledger Model. In 5th International Workshop on Formal Methods for Blockchains (FMBC 2024). Open Access Series in Informatics (OASIcs), Volume 118, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/OASIcs.FMBC.2024.10

Abstract

Blockchain ledgers based on the extended UTxO model support fully expressive smart contracts to specify permissions for performing certain actions, such as spending transaction outputs or minting assets. There have been some attempts to standardize the implementation of stateful programs using this infrastructure, with varying degrees of success. To remedy this, we introduce the framework of structured contracts to formalize what it means for a stateful program to be correctly implemented on the ledger. Using small-step semantics, our approach relates low-level ledger transitions to high-level transitions of the smart contract being specified, thus allowing users to prove that their abstract specification is adequately realized on the blockchain. We argue that the framework is versatile enough to cover a range of examples, in particular proving the equivalence of multiple concrete implementations of the same abstract specification. Building upon prior meta-theoretical results, our results have been mechanized in the Agda proof assistant, paving the way to rigorous verification of smart contracts.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program specifications
  • Security and privacy → Formal methods and theory of security
Keywords
  • blockchain
  • ledger
  • smart contract
  • formal verification
  • specification
  • transition systems
  • Agda
  • UTxO
  • EUTxO
  • small-step semantics

Metrics

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

Supplementary Materials

References

  1. Arnaud Bailly. Model-based testing with QuickCheck, 2022. URL: https://engineering.iog.io/2022-09-28-introduce-q-d/.
  2. Massimo Bartoletti, Letterio Galletta, and Maurizio Murgia. A theory of transaction parallelism in blockchains. Logical Methods in Computer Science, Volume 17, Issue 4, nov 2021. URL: https://doi.org/10.46298/lmcs-17(4:10)2021.
  3. Massimo Bartoletti, Stefano Lande, Maurizio Murgia, and Roberto Zunino. Verification of recursive bitcoin contracts. CoRR, abs/2011.14165, 2020. URL: https://doi.org/10.48550/arXiv.2011.14165.
  4. Massimo Bartoletti, Riccardo Marchesin, and Roberto Zunino. Secure compilation of rich smart contracts on poor UTXO blockchains, 2023. URL: https://doi.org/10.48550/arXiv.2305.09545.
  5. Massimo Bartoletti and Roberto Zunino. BitML: a calculus for Bitcoin smart contracts. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, pages 83-100. ACM, 2018. URL: https://doi.org/10.1145/3243734.3243795.
  6. Vitalik Buterin. Ethereum: A Next-Generation Smart Contract and Decentralized Application Platform. https://ethereum.org/en/whitepaper/, 2014.
  7. 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.
  8. Manuel M. T. Chakravarty, James Chapman, Kenneth MacKenzie, Orestis Melkonian, Jann Müller, Michael Peyton Jones, Polina Vinogradova, Philip Wadler, and Joachim Zahnentferner. UTXO_ma: UTXO with multi-asset support. 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 112-130. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-61467-6_8.
  9. Manuel M. T. Chakravarty, James Chapman, Kenneth MacKenzie, Orestis Melkonian, Michael Peyton Jones, and Philip Wadler. The Extended UTxO model. In Proceedings of Trusted Smart Contracts (WTSC), volume 12063 of LNCS. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-54455-3_37.
  10. Manuel M. T. Chakravarty, Sandro Coretti, Matthias Fitzi, Peter Gazi, Philipp Kant, Aggelos Kiayias, and Alexander Russell. Hydra: Fast isomorphic state channels. IACR Cryptol. ePrint Arch., 2020:299, 2020. URL: https://eprint.iacr.org/2020/299.
  11. Florent Chevrou. A journey through the auditing process of a smart contract, 2023. URL: https://www.tweag.io/blog/2023-05-11-audit-smart-contract/.
  12. Jared Corduan, Matthias Güdemann, and Polina Vinogradova. A Formal Specification of the Cardano Ledger. https://github.com/input-output-hk/cardano-ledger/releases/latest/download/shelley-ledger.pdf, 2019.
  13. Ergo Team. Ergo: A Resilient Platform For Contractual Money. https://whitepaper.io/document/753/ergo-1-whitepaper, 2019.
  14. Ilya Sergey et al. Safer smart contract programming with Scilla. In Proceedings of the ACM on Programming Languages, volume 3 (OOPSLA), pages 1-30. ACM, 2019. URL: https://doi.org/10.1145/3360611.
  15. Pablo Lamela Seijas et al. Marlowe: Implementing and analysing financial contracts on blockchain. In Financial Cryptography and Data Security, pages 496-511, Cham, 2020. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-54455-3_35.
  16. Ethereum Team. ERC-721 TOKEN STANDARD. https://ethereum.org/en/developers/docs/standards/tokens/erc-721, 2023.
  17. LM Goodman. Tezos - a self-amending crypto-ledger (white paper), 2014. Google Scholar
  18. Tobias Guggenberger, Vincent Schlatt, Jonathan Schmid, and Nils Urbach. A structured overview of attacks on blockchain systems. PACIS, page 100, 2021. URL: https://aisel.aisnet.org/pacis2021/100.
  19. Jiao Jiao, Shuanglong Kan, Shang-Wei Lin, David Sanan, Yang Liu, and Jun Sun. Semantic understanding of smart contracts: Executable operational semantics of Solidity. In 2020 IEEE Symposium on Security and Privacy (SP), pages 1695-1712, 2020. URL: https://doi.org/10.1109/SP40000.2020.00066.
  20. Andre Knispel and Polina Vinogradova. A Formal Specification of the Cardano Ledger integrating Plutus Core. https://github.com/input-output-hk/cardano-ledger/releases/latest/download/alonzo-ledger.pdf, 2021.
  21. Diego Marmsoler and Achim D. Brucker. A denotational semantics of Solidity in Isabelle/HOL. In Software Engineering and Formal Methods: 19th International Conference, SEFM 2021, Virtual Event, December 6–10, 2021, Proceedings, pages 403-422, Berlin, Heidelberg, 2021. Springer-Verlag. URL: https://doi.org/10.1007/978-3-030-92124-8_23.
  22. Anastasia Mavridou, Aron Laszka, Emmanouela Stachtiari, and Abhishek Dubey. VeriSolid: Correct-by-design smart contracts for Ethereum. In International Conference on Financial Cryptography and Data Security, pages 446-465. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-32101-7_27.
  23. Robin Milner. Communicating and mobile systems: the π-calculus. Cambridge University Press, 1999. Google Scholar
  24. S. Nakamoto. Bitcoin: A Peer-to-Peer Electronic Cash System. https://bitcoin.org/en/bitcoin-paper, oct 2008.
  25. Ulf Norell. Dependently typed programming in Agda. In International School on Advanced Functional Programming, pages 230-266. Springer, 2008. URL: https://doi.org/10.1007/978-3-642-04652-0_5.
  26. George Pitrlea, Amrit Kumar, and Ilya Sergey. Practical smart contract sharding with ownership and commutativity analysis. In PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 2021, PLDI 2021, pages 1327-1341, New York, NY, USA, 2021. Association for Computing Machinery. URL: https://doi.org/10.1145/3453483.3454112.
  27. Grigore Roşu and Traian Şerbănuţă. An overview of the K semantic framework. The Journal of Logic and Algebraic Programming, 79:397-434, aug 2010. URL: https://doi.org/10.1016/j.jlap.2010.03.012.
  28. Runtime Verification Team. Smart contract analysis and verification, 2023. URL: https://runtimeverification.com/smartcontract.
  29. The ZILLIQA Team. The ZILLIQA Technical Whitepaper. https://docs.zilliqa.com/whitepaper.pdf, 2017.
  30. The Solidity Authors. Solidity 0.8.25 documentation. https://docs.soliditylang.org/en/v0.8.25/, 2023.
  31. Jan Xie. Nervos CKB: A Common Knowledge Base for Crypto-Economy. https://github.com/nervosnetwork/rfcs/blob/master/rfcs/0002-ckb/0002-ckb.md, 2018.
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