Document Open Access Logo

Verification of Bitcoin Script in Agda Using Weakest Preconditions for Access Control

Authors Fahad F. Alhabardi , Arnold Beckmann , Bogdan Lazar, Anton Setzer

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2021.1.pdf
  • Filesize: 0.81 MB
  • 25 pages

Document Identifiers

Author Details

Fahad F. Alhabardi
  • Dept. of Computer Science, Swansea University, UK
Arnold Beckmann
  • Dept. of Computer Science, Swansea University, UK
Bogdan Lazar
  • University of Bath, UK
Anton Setzer
  • Dept. of Computer Science, Swansea University, UK

Funding

  • Alhabardi, Fahad F.: Supported by Saudi Arabia Cultural Bureau in London.
  • Setzer, Anton: Supported by COST actions CA20111 EuroProofNet and CA15123 EU Types.

Acknowledgements

We would like to thank the anonymous referees for valuable comments and suggestions.

Cite AsGet BibTex

Fahad F. Alhabardi, Arnold Beckmann, Bogdan Lazar, and Anton Setzer. Verification of Bitcoin Script in Agda Using Weakest Preconditions for Access Control. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 1:1-1:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.TYPES.2021.1

Abstract

This paper contributes to the verification of programs written in Bitcoin’s smart contract language script in the interactive theorem prover Agda. It focuses on the security property of access control for script programs that govern the distribution of Bitcoins. It advocates that weakest preconditions in the context of Hoare triples are the appropriate notion for verifying access control. It aims at obtaining human-readable descriptions of weakest preconditions in order to close the validation gap between user requirements and formal specification of smart contracts. As examples for the proposed approach, the paper focuses on two standard script programs that govern the distribution of Bitcoins, Pay to Public Key Hash (P2PKH) and Pay to Multisig (P2MS). The paper introduces an operational semantics of the script commands used in P2PKH and P2MS, which is formalised in the Agda proof assistant and reasoned about using Hoare triples. Two methodologies for obtaining human-readable descriptions of weakest preconditions are discussed: (1) a step-by-step approach, which works backwards instruction by instruction through a script, sometimes grouping several instructions together; (2) symbolic execution of the code and translation into a nested case distinction, which allows to read off weakest preconditions as the disjunction of conjunctions of conditions along accepting paths. A syntax for equational reasoning with Hoare Triples is defined in order to formalise those approaches in Agda.

Subject Classification

ACM Subject Classification
  • Theory of computation → Hoare logic
  • Theory of computation → Type theory
  • Theory of computation → Programming logic
  • Theory of computation → Interactive proof systems
  • Theory of computation → Operational semantics
  • Theory of computation → Denotational semantics
  • Security and privacy → Access control
  • Security and privacy → Logic and verification
  • Applied computing → Digital cash
Keywords
  • Blockchain
  • Cryptocurrency
  • Bitcoin
  • Agda
  • Verification
  • Hoare logic
  • Bitcoin Script
  • P2PKH
  • P2MS
  • Access control
  • Weakest precondition
  • Predicate transformer semantics
  • Provable correctness
  • Symbolic execution
  • Smart contracts

Metrics

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

Related Versions

Supplementary Materials

References

  1. Adacore. SPARK 2014, retrieved 9 november 2021. URL: https://www.adacore.com/about-spark.
  2. Agda Team. Agda documentation, retrieved 21 april 2022. URL: https://agda.readthedocs.io/en/latest/index.html.
  3. Agda Team. Agda Reflection, retrieved 21 april 2022. URL: https://agda.readthedocs.io/en/latest/language/reflection.html.
  4. Mouhamad Almakhour, Layth Sliman, Abed Ellatif Samhat, and Abdelhamid Mellouk. Verification of smart contracts: A survey. Pervasive and Mobile Computing, 67:1-19, 2020. URL: https://doi.org/10.1016/j.pmcj.2020.101227.
  5. Sidney Amani, Myriam Bégel, Maksym Bortin, and Mark Staples. Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, pages 66-77, New York, NY, USA, 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3167084.
  6. Andreas M Antonopoulos. Mastering Bitcoin: Programming the open blockchain (Second ed.). O'Reilly Media, Inc., 2017. Google Scholar
  7. Nicola Atzei, Massimo Bartoletti, Stefano Lande, and Roberto Zunino. A formal model of bitcoin transactions. In Financial Cryptography and Data Security, pages 541-560, Berlin, Heidelberg, 2018. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-662-58387-6_29.
  8. 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, CCS '18, pages 83-100, New York, NY, USA, 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3243734.3243795.
  9. Bruno Bernardo, Raphaël Cauderlier, Zhenlei Hu, Basile Pesin, and Julien Tesson. Mi-Cho-Coq, a Framework for Certifying Tezos Smart Contracts. In Formal Methods. FM 2019 International Workshops, pages 368-379, Cham, 2020. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-54994-7_28.
  10. Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Anitha Gollamudi, Georges Gonthier, Nadim Kobeissi, Natalia Kulatova, Aseem Rastogi, Thomas Sibut-Pinote, Nikhil Swamy, and Santiago Zanella-Béguelin. Formal Verification of Smart Contracts: Short Paper. In Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security, PLAS '16, pages 91-96, New York, NY, USA, 2016. Association for Computing Machinery. URL: https://doi.org/10.1145/2993600.2993611.
  11. Bitcoin Community. Welcome to the Bitcoin Wiki. Availabe from https://en.bitcoin.it/wiki/Script, 2010.
  12. Ana Bove, Peter Dybjer, and Ulf Norell. A Brief Overview of Agda - A Functional Language with Dependent Types. In Theorem Proving in Higher Order Logics, pages 73-7, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-03359-9_6.
  13. Vitalik Buterin. Ethereum: A next-generation smart contract and decentralized application platform, 2014. URL: https://ethereum.org/en/whitepaper.
  14. 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 Leveraging Applications of Formal Methods, Verification and Validation: Applications, pages 89-111, Cham, 2020. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-61467-6_7.
  15. Manuel M. T. Chakravarty, James Chapman, Kenneth MacKenzie, Orestis Melkonian, Jann Müller, Michael Peyton Jones, Polina Vinogradova, Philip Wadler, and Joachim Zahnentferner. UTXOma: UTXO with Multi-asset Support. In Leveraging Applications of Formal Methods, Verification and Validation: Applications, pages 112-130, Cham, 2020. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-61467-6_8.
  16. Manuel M. T. Chakravarty, James Chapman, Kenneth MacKenzie, Orestis Melkonian, Michael Peyton Jones, and Philip Wadler. The Extended UTXO Model. In Financial Cryptography and Data Security, pages 525-539, Cham, 2020. Springer International Publishing. Google Scholar
  17. James Chapman, Roman Kireev, Chad Nester, and Philip Wadler. System F in Agda, for Fun and Profit. In Mathematics of Program Construction, pages 255-297, Cham, 2019. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-33636-3_10.
  18. Martin Churchill, Peter D. Mosses, Neil Sculthorpe, and Paolo Torrini. Reusable components of semantic specifications. In Shigeru Chiba, Éric Tanter, Erik Ernst, and Robert Hirschfeld, editors, Transactions on Aspect-Oriented Software Development XII, pages 132-179, Berlin, Heidelberg, 2015. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-662-46734-3_4.
  19. Edmund M. Clarke and Jeannette M. Wing. Formal methods: State of the art and future directions. ACM Comput. Surv., 28(4):626-643, December 1996. URL: https://doi.org/10.1145/242223.242257.
  20. crypto.stackexchange. Is there any famous protocol that were proven secure but whose proof was wrong and lead to real world attacks?, retrieved 22 april 2022. URL: https://crypto.stackexchange.com/questions/98829/is-there-any-famous-protocol-that-were-proven-secure-but-whose-proof-was-wrong-a.
  21. Peter D and Mosses. Modular structural operational semantics. Journal of Logic and Algebraic Programming, 60-61(0):195-228, 2004. URL: https://doi.org/10.1016/j.jlap.2004.03.008.
  22. Edsger W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM, 18(8):453-457, August 1975. URL: https://doi.org/10.1145/360933.360975.
  23. Etherscan. TheDAO smart contract 2016, retrieved 27 march 2022. Availabe from http://etherscan.io/address/0xbb9bc244d798123fde783fcc1c72d3bb8c189413#code.
  24. Jean-Christophe Filliâtre and Andrei Paskevich. Why3 - Where Programs Meet Provers. In Programming Languages and Systems, pages 125-128, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-37036-6_8.
  25. Yoichi Hirai. Defining the Ethereum Virtual Machine for Interactive Theorem Provers. In Financial Cryptography and Data Security, pages 520-535, Cham, 2017. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-70278-0_33.
  26. C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576-585, October 1969. URL: https://doi.org/10.1145/363235.363259.
  27. IMDEA Software Institute. HTT: Hoare Type Theory, 10 march 2015. Available from URL: https://software.imdea.org/~aleks/htt/.
  28. Sukrit Kalra, Seep Goel, Mohan Dhawan, and Subodh Sharma. ZEUS: Analyzing Safety of Smart Contracts. In 25th Annual Network and Distributed System Security Symposium, NDSS 2018, San Diego, California, USA, February 18-21, 2018, pages 1-15. The Internet Society, 2018. URL: https://doi.org/10.14722/ndss.2018.23082.
  29. James C. King. Symbolic execution and program testing. Commun. ACM, 19(7):385-394, July 1976. URL: https://doi.org/10.1145/360248.360252.
  30. Rick Klomp and Andrea Bracciali. On Symbolic Verification of Bitcoin’s script Language. In Data Privacy Management, Cryptocurrencies and Blockchain Technology, pages 38-56, Cham, 2018. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-00305-0_3.
  31. Loi Luu, Duc-Hiep Chu, Hrishi Olickel, Prateek Saxena, and Aquinas Hobor. Making Smart Contracts Smarter. In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, CCS '16, pages 254-269, New York, NY, USA, 2016. Association for Computing Machinery. URL: https://doi.org/10.1145/2976749.2978309.
  32. Luiz Eduardo G. Martins and Tony Gorschek. Requirements engineering for safety-critical systems: Overview and challenges. IEEE Software, 34(4):49-57, 2017. URL: https://doi.org/10.1109/MS.2017.94.
  33. Anastasia Mavridou, Aron Laszka, Emmanouela Stachtiari, and Abhishek Dubey. VeriSolid: Correct-by-Design Smart Contracts for Ethereum. In Financial Cryptography and Data Security, pages 446-465, Cham, 2019. Springer International Publishing. Google Scholar
  34. Orestis Melkonian. Formalizing BitML Calculus in Agda, 2019. Student Research Competition, Poster Session, ICFP'19. URL: https://omelkonian.github.io/data/publications/formal-bitml.pdf.
  35. Orestis Melkonian. Formalizing Extended UTxO and BitML Calculus in Agda. Master’s thesis, Utrecht University, Department of Information and Computing Sciences, July 2019. URL: https://studenttheses.uu.nl/handle/20.500.12932/32981.
  36. Dominic P. Mulligan, Scott Owens, Kathryn E. Gray, Tom Ridge, and Peter Sewell. Lem: Reusable engineering of real-world semantics. ACM SIGPLAN Notices, 49(9):175-188, August 2014. URL: https://doi.org/10.1145/2692915.2628143.
  37. Yvonne Murray and David A. Anisi. Survey of Formal Verification Methods for Smart Contracts on Blockchain. In 2019 10th IFIP International Conference on New Technologies, Mobility and Security (NTMS), pages 1-6, 2019. URL: https://doi.org/10.1109/NTMS.2019.8763832.
  38. Satoshi Nakamoto. Bitcoin: A peer-to-peer electronic cash system. Decentralized Business Review, 2008. URL: https://www.debr.io/article/21260.pdf.
  39. Nanevski, Aleksandar and Vafeiadis, Viktor and Berdine, Josh. Structuring the Verification of Heap-Manipulating Programs. SIGPLAN Not., 45(1):261-274, January 2010. URL: https://doi.org/10.1145/1707801.1706331.
  40. Ulf Norell. Dependently typed programming in Agda. In Advanced Functional Programming: 6th International School, AFP 2008, Heijen, The Netherlands, May 2008, Revised Lectures, pages 230-266, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-04652-0_5.
  41. Russell O'Connor. Simplicity: A new language for blockchains. In Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security, PLAS '17, pages 107-120, New York, NY, USA, 2017. Association for Computing Machinery. URL: https://doi.org/10.1145/3139337.3139340.
  42. Daejun Park, Yi Zhang, Manasvi Saxena, Philip Daian, and Grigore Roşu. A Formal Verification Tool for Ethereum VM Bytecode. In Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2018, pages 912-915, New York, NY, USA, 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3236024.3264591.
  43. Christine Paulin-Mohring. Introduction to the Coq Proof-Assistant for Practical Software Verification, pages 45-95. Springer Berlin Heidelberg, Berlin, Heidelberg, 2012. URL: https://doi.org/10.1007/978-3-642-35746-6_3.
  44. Elizabeth D. Rather, Donald R. Colburn, and Charles H. Moore. The Evolution of Forth, pages 625-670. Association for Computing Machinery, New York, NY, USA, 1996. URL: https://doi.org/10.1145/234286.1057832.
  45. Maria Ribeiro, Pedro Adão, and Paulo Mateus. Formal Verification of Ethereum Smart Contracts Using Isabelle/HOL, pages 71-97. Springer International Publishing, Cham, 2020. URL: https://doi.org/10.1007/978-3-030-62077-6_7.
  46. Anton Setzer. Modelling Bitcoin in Agda. CoRR, abs/1804.06398, 2018. URL: http://arxiv.org/abs/1804.06398.
  47. Anton Setzer, Fahad Alhabardi, and Bogdan Lazar. Verification Of Smart Contracts With Agda. Available from https://github.com/fahad1985lab/Smart--Contracts--Verification--With--Agda, 2021.
  48. Stack Exchange Inc. provable security - Is there any famous protocol that were proven secure but whose proof was wrong and lead to real world attacks? , retrieved 22 april 2022. Availabe from URL: https://crypto.stackexchange.com/questions/98829/is-there-any-famous-protocol-that-were-proven-secure-but-whose-proof-was-wrong-a.
  49. Philip Wadler, Wen Kokke, and Jeremy G. Siek. Programming Language Foundations in Agda. Online textbook, July 2020. URL: https://plfa.github.io/Equality/.
  50. Maximilian Wohrer and Uwe Zdun. Smart Contracts: Security Patterns in the Ethereum Ecosystem and Solidity. In 2018 International Workshop on Blockchain Oriented Software Engineering (IWBOSE), pages 2-8, 2018. URL: https://doi.org/10.1109/IWBOSE.2018.8327565.
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