Document Open Access Logo

Towards Mechanised Consensus in Isabelle

Authors Elliot Jones, Diego Marmsoler

PDF
Thumbnail PDF

File

OASIcs.FMBC.2024.4.pdf
  • Filesize: 0.7 MB
  • 22 pages

Document Identifiers

Author Details

Elliot Jones
  • Department of Computer Science, University of Exeter, UK
Diego Marmsoler
  • Department of Computer Science, University of Exeter, UK

Funding

  • Marmsoler, Diego: This work was supported by the Engineering and Physical Sciences Research Council [grant number EP/X027619/1].

Acknowledgements

We would like to thank the FMBC 2024 reviewers for the careful reading and constructive suggestions on the paper and the formalisation.

Cite AsGet BibTex

Elliot Jones and Diego Marmsoler. Towards Mechanised Consensus in Isabelle. In 5th International Workshop on Formal Methods for Blockchains (FMBC 2024). Open Access Series in Informatics (OASIcs), Volume 118, pp. 4:1-4:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/OASIcs.FMBC.2024.4

Abstract

A blockchain acts as a universal ledger for digital transactions between two parties that require no moderation from a third party. Such transactions are cheaper, quicker, and more secure with high traceability and transparency, with the decentralised structure of a blockchain network allowing for greater scalability and availability. For these reasons, blockchain is at the forefront of emerging technologies, with a wide variety of industries investing billions into the technology. A blockchains consensus protocol is what allows a blockchain network to be decentralised but can be subject to malicious behaviour and faults in its design and implementation that can lead to catastrophic effects like the DAO hack that resulted in a loss of $60 million. From this it is clear to see that the verifications of these protocols are paramount to ensure the safe use of blockchain. In this research, we formally verify the Proof-of-Work consensus protocol, used by Bitcoin, in Isabelle/HOL by modelling the blockchain as the longest branch in a binary tree and proving that the common prefix property holds with the assumption that the network is in majority honest. In this paper, we discuss the validity of our approach, key functions and lemmas we used to complete the proof, advantages and drawbacks of the model, related work and how this research can be taken further.

Subject Classification

ACM Subject Classification
  • Security and privacy → Logic and verification
Keywords
  • Formal Methods
  • Blockchain
  • Isabelle/HOL
  • Consensus
  • Verification
  • Theorem Provers

Metrics

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

Supplementary Materials

References

  1. Musab A Alturki, Jing Chen, Victor Luchangco, Brandon Moore, Karl Palmskog, Lucas Peña, and Grigore Roşu. Towards a verified model of the algorand consensus protocol in coq. In Formal Methods. FM 2019 International Workshops: Porto, Portugal, October 7-11, 2019, Revised Selected Papers, Part I 3, pages 362-367. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-54994-7_27.
  2. Musab A Alturki, Elaine Li, Daejun Park, Brandon Moore, Karl Palmskog, Lucas Pena, and Grigore Roşu. Verifying gasper with dynamic validator sets in coq. Technical report, 2020. Google Scholar
  3. 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: 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings 22, pages 73-78. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03359-9_6.
  4. Sean Braithwaite, Ethan Buchman, Igor V. Konnov, Zarko Milosevic, Ilina Stoilkovska, Josef Widder, and Anca Zamfir. Formal specification and model checking of the tendermint blockchain synchronization protocol (short paper). In FMBC@CAV, 2020. URL: https://doi.org/10.4230/OASIcs.FMBC.2020.10.
  5. Hao Bu and Meng Sun. Towards modeling and verification of the ckb block synchronization protocol in coq. In Formal Methods and Software Engineering: 22nd International Conference on Formal Engineering Methods, ICFEM 2020, Singapore, Singapore, March 1-3, 2021, Proceedings 22, pages 287-296. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-63406-3_17.
  6. Harold Carr, Christa Jenkins, Mark Moir, Victor Cacciari Miraldo, and Lisandra Silva. Towards formal verification of hotstuff-based byzantine fault tolerant consensus in agda. In Jyotirmoy V. Deshmukh, Klaus Havelund, and Ivan Perez, editors, NASA Formal Methods, pages 616-635, Cham, 2022. Springer International Publishing. URL: https://doi.org/10.1007/978-3-031-06773-0_33.
  7. Franck Cassez, Joanne Fuller, and Aditya Asgaonkar. Formal verification of the ethereum 2.0 beacon chain. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 167-182. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-99524-9_9.
  8. Coindesk. How the dao hack changed ethereum and crypto, 2023. [Accessed December 2023]. URL: https://www.coindesk.com/consensus-magazine/2023/05/09/coindesk-turns-10-how-the-dao-hack-changed-ethereum-and-crypto/.
  9. CoinMarketCap. Bitcoin market capitalization, 2023. [Accessed December 2023]. URL: https://coinmarketcap.com/currencies/bitcoin/.
  10. Phil Daian, Rafael Pass, and Elaine Shi. Snow white: Robustly reconfigurable consensus and applications to provably secure proof of stake. In Ian Goldberg and Tyler Moore, editors, Financial Cryptography and Data Security, pages 23-41, Cham, 2019. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-32101-7_2.
  11. Forkast. How ethereum classic’s 51% attacks reveal risks to bitcoin and ethereum, 2020. [Accessed December 2023]. URL: https://forkast.news/video-audio/ethereum-classic-repeat-hacks-etc-labs-ceo-terry-culver-ben-sauter/.
  12. Juan Garay, Aggelos Kiayias, and Nikos Leonardos. The bitcoin backbone protocol: Analysis and applications. In Annual international conference on the theory and applications of cryptographic techniques, pages 281-310. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-46803-6_10.
  13. Growjo. Certik revenue and competitors, 2022. [Accessed December 2023]. URL: https://growjo.com/company/CertiK.
  14. Yoichi Hirai. A repository for pos related formal methods. https://github.com/palmskog/pos, 2018. Google Scholar
  15. Mauro Jaskelioff and Stephan Merz. Proving the correctness of disk paxos. Archive of Formal Proofs, jun 2005. , Formal proof development. URL: https://isa-afp.org/entries/DiskPaxos.html.
  16. Elliot Jones and Diego Marmsoler. Towards Mechanised Consensus in Isabelle. version 1.0., (visited on 02/05/2024). URL: https://doi.org/10.5281/zenodo.10479776.
  17. Florian Kammüller and Uwe Nestmann. Inter-Blockchain Protocols with the Isabelle Infrastructure Framework. In Bruno Bernardo and Diego Marmsoler, editors, 2nd Workshop on Formal Methods for Blockchains (FMBC 2020), volume 84 of Open Access Series in Informatics (OASIcs), pages 11:1-11:12, Dagstuhl, Germany, 2020. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/OASIcs.FMBC.2020.11.
  18. Aggelos Kiayias, Alexander Russell, Bernardo David, and Roman Oliynykov. Ouroboros: A provably secure proof-of-stake blockchain protocol. In Annual international cryptology conference, pages 357-388. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63688-7_12.
  19. Philipp Küfner, Uwe Nestmann, and Christina Rickmann. Formal verification of distributed algorithms. In Jos C. M. Baeten, Tom Ball, and Frank S. de Boer, editors, Theoretical Computer Science, pages 209-224, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-33475-7_15.
  20. Giuliano Losa and Mike Dodds. On the Formal Verification of the Stellar Consensus Protocol. In Bruno Bernardo and Diego Marmsoler, editors, 2nd Workshop on Formal Methods for Blockchains (FMBC 2020), volume 84 of Open Access Series in Informatics (OASIcs), pages 9:1-9:9, Dagstuhl, Germany, 2020. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/OASIcs.FMBC.2020.9.
  21. Xiaokun Luan and Meng Sun. Modeling and verification of ckb consensus protocol in coq. In 2021 IEEE 21st International Conference on Software Quality, Reliability and Security Companion (QRS-C), pages 660-667. IEEE, 2021. URL: https://doi.org/10.1109/QRS-C55045.2021.00100.
  22. Bojan Marinković, Paola Glavan, Zoran Ognjanović, Dragan Doder, and Thomas Studer. Probabilistic consensus of the blockchain protocol. In Gabriele Kern-Isberner and Zoran Ognjanović, editors, Symbolic and Quantitative Approaches to Reasoning with Uncertainty, pages 469-480, Cham, 2019. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-29765-7_39.
  23. Diego Marmsoler. Towards verified blockchain architectures: A case study on interactive architecture verification. In Formal Techniques for Distributed Objects, Components, and Systems: 39th IFIP WG 6.1 International Conference, FORTE 2019, Held as Part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Kongens Lyngby, Denmark, June 17–21, 2019, Proceedings, pages 204-223, Berlin, Heidelberg, 2019. Springer-Verlag. URL: https://doi.org/10.1007/978-3-030-21759-4_12.
  24. Diego Marmsoler and Habtom Kashay Gidey. Interactive verification of architectural design patterns in factum. Form. Asp. Comput., 31(5):541-610, nov 2019. URL: https://doi.org/10.1007/s00165-019-00488-x.
  25. Ahmed Afif Monrat, Olov Schelén, and Karl Andersson. A survey of blockchain from the perspectives of applications, challenges, and opportunities. IEEE Access, 7:117134-117151, 2019. URL: https://doi.org/10.1109/ACCESS.2019.2936094.
  26. Neptune Mutual. Ethereum classic 51% attacks, 2023. [Accessed December 2023]. URL: https://neptunemutual.com/blog/ethereum-classic-51-attacks/.
  27. Satoshi Nakamoto. Bitcoin: A peer-to-peer electronic cash system. Decentralized business review, 2008. Google Scholar
  28. R. Nakamura, T. Jimba, and D. Harz. Refinement and verification of cbc casper. In 2019 Crypto Valley Conference on Blockchain Technology (CVCBT), pages 26-38, Los Alamitos, CA, USA, jun 2019. IEEE Computer Society. URL: https://doi.org/10.1109/CVCBT.2019.00008.
  29. Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson. Isabelle/HOL: a proof assistant for higher-order logic. Springer, 2002. URL: https://doi.org/10.1007/3-540-45949-9.
  30. Karl Palmskog, Milos Gligoric, Lucas Pena, Brandon Moore, and Grigore Roşu. Verification of casper in the coq proof assistant. Technical report, University of Illinois at Urbana-Champaign, 2018. Google Scholar
  31. Rafael Pass, Lior Seeman, and Abhi Shelat. Analysis of the blockchain protocol in asynchronous networks. In Jean-Sébastien Coron and Jesper Buus Nielsen, editors, Advances in Cryptology - EUROCRYPT 2017, pages 643-673, Cham, 2017. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-56614-6_22.
  32. George Pîrlea and Ilya Sergey. Mechanising blockchain consensus. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 78-90, 2018. URL: https://doi.org/10.1145/3167086.
  33. Vincent Rahli, Ivana Vukotic, Marcus Völp, and Paulo Esteves-Verissimo. Velisarios: Byzantine fault-tolerant protocols powered by coq. In Amal Ahmed, editor, Programming Languages and Systems, pages 619-650, Cham, 2018. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-89884-1_22.
  34. Statista. Blockchain - statistics and facts, 2023. [Accessed December 2023]. URL: https://www.statista.com/statistics/800426/worldwide-blockchain-solutions-spending/.
  35. The Coq Development Team. The Coq reference manual - release 8.18.0. https://coq.inria.fr/doc/V8.18.0/refman, 2023.
  36. Søren Eller Thomsen and Bas Spitters. Formalizing nakamoto-style proof of stake. In 2021 IEEE 34th Computer Security Foundations Symposium (CSF), pages 1-15. IEEE, 2021. URL: https://doi.org/10.1109/CSF51468.2021.00042.
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact