Document Open Access Logo

A Proof-Producing Compiler for Blockchain Applications

Authors Jeremy Avigad , Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman

PDF
Thumbnail PDF

File

LIPIcs.ITP.2023.7.pdf
  • Filesize: 0.64 MB
  • 19 pages

Document Identifiers

Author Details

Jeremy Avigad
  • Carnegie Mellon University, Pittsburgh, PA, USA
Lior Goldberg
  • StarkWare Industries Ltd., Netanya, Israel
David Levit
  • StarkWare Industries Ltd., Netanya, Israel
Yoav Seginer
  • Amsterdam, Netherlands
Alon Titelman
  • StarkWare Industries Ltd., Netanya, Israel

Acknowledgements

We are grateful to the Lean developers and the Lean community for providing infrastructure for this project, and to three anonymous reviewers for numerous corrections and improvements.

Cite As Get BibTex

Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, and Alon Titelman. A Proof-Producing Compiler for Blockchain Applications. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.ITP.2023.7

Abstract

Cairo is a programming language for running decentralized applications (dapps) at scale. Programs written in the Cairo language are compiled to machine code for the Cairo CPU architecture, and cryptographic protocols are used to verify the results of the execution traces efficiently on blockchain. We explain how we have extended the Cairo compiler with tooling that enables users to prove, in the Lean 3 proof assistant, that compiled code satisfies high-level functional specifications. We demonstrate the success of our approach by verifying primitives for computations with an elliptic curve over a large finite field, as well as their use in the validation of cryptographic signatures.

Subject Classification

ACM Subject Classification
  • General and reference → Verification
  • Theory of computation → Logic and verification
  • Software and its engineering → Semantics
Keywords
  • formal verification
  • smart contracts
  • interactive proof systems

Metrics

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

Supplementary Materials

References

  1. Oskar Abrahamsson, Son Ho, Hrutvik Kanabar, Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Yong Kiam Tan. Proof-producing synthesis of CakeML from monadic HOL functions. J. Autom. Reason., 64(7):1287-1306, 2020. URL: https://doi.org/10.1007/s10817-020-09559-8.
  2. Frances E. Allen. Control flow analysis. SIGPLAN Notices., 5(7):1-19, July 1970. URL: https://doi.org/10.1145/390013.808479.
  3. David Kurniadi Angdinata and Junyan Xu. An elementary formal proof of the group law on weierstrass elliptic curves in any characteristic. In Adam Naumowicz and René Thiemann, editors, Interactive Theorem Proving (ITP) 2023, 2023. Google Scholar
  4. Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, and Alon Titelman. A verified algebraic representation of Cairo program execution. In Andrei Popescu and Steve Zdancewic, editors, Certified Programs and Proofs (CPP) 2022, pages 153-165. ACM, 2022. URL: https://doi.org/10.1145/3497775.3503675.
  5. Evmorfia-Iro Bartzia and Pierre-Yves Strub. A formal library for elliptic curves in the Coq proof assistant. In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving (ITP) 2014, pages 77-92. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08970-6_6.
  6. Eli Ben-Sasson, Iddo Bentov, Yinon Horesh, and Michael Riabzev. Scalable, transparent, and post-quantum secure computational integrity. IACR Cryptol. ePrint Arch., 2018:46, 2018. URL: http://eprint.iacr.org/2018/046.
  7. Mario Carneiro. Metamath Zero: Designing a theorem prover prover. In Christoph Benzmüller and Bruce R. Miller, editors, Intelligent Computer Mathematics (CICM) 2020, pages 71-88. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-53518-6_5.
  8. Adam Chlipala. The Bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier. In Greg Morrisett and Tarmo Uustalu, editors, International Conference on Functional Programming (ICFP) 2013, pages 391-402. ACM, 2013. URL: https://doi.org/10.1145/2500365.2500592.
  9. Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean theorem prover (system description). In Amy P. Felty and Aart Middeldorp, editors, Conference on Automated Deduction (CADE) 2015, pages 378-388. Springer, Berlin, 2015. URL: https://doi.org/10.1007/978-3-319-21401-6_26.
  10. Edsger W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM, 18(8):453-457, 1975. URL: https://doi.org/10.1145/360933.360975.
  11. Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, and Adam Chlipala. Simple high-level code for cryptographic arithmetic: With proofs, without compromises. ACM SIGOPS Oper. Syst. Rev., 54(1):23-30, 2020. URL: https://doi.org/10.1145/3421473.3421477.
  12. Andrew Erbsen. Crafting Certified Elliptic Curve Cryptography Implementations in Coq. PhD thesis, Massachusetts Institute of Technology, 2017. Google Scholar
  13. Jean-Christophe Filliâtre and Andrei Paskevich. Why3 - Where programs meet provers. In Matthias Felleisen and Philippa Gardner, editors, European Symposium on Programming (ESOP) 2013: Programming Languages and Systems, pages 125-128. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-37036-6_8.
  14. Lior Goldberg, Shahar Papini, and Michael Riabzev. Cairo - a Turing-complete STARK-friendly CPU architecture. Cryptology ePrint Archive, Report 2021/1063, 2021. URL: https://ia.cr/2021/1063.
  15. Thomas C. Hales and Rodrigo Raya. Formal proof of the group law for edwards elliptic curves. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, International Joint Conference on Automated Reasoning (IJCAR) 2020, pages 254-269. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51054-1_15.
  16. StarkWare Industries. Cairo. URL: https://www.cairo-lang.org/.
  17. Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. CakeML: a verified implementation of ML. In Suresh Jagannathan and Peter Sewell, editors, Principles of Programming Languages (POPL) 2014, pages 179-192. ACM, 2014. URL: https://doi.org/10.1145/2535838.2535841.
  18. K. Rustan M. Leino. Dafny: An automatic program verifier for functional correctness. In Edmund M. Clarke and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR) 2010- 16th, pages 348-370. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-17511-4_20.
  19. Xavier Leroy. Formal verification of a realistic compiler. Commun. ACM, 52(7):107-115, 2009. URL: https://doi.org/10.1145/1538788.1538814.
  20. The mathlib community. The Lean mathematical library. In Jasmin Blanchette and Catalin Hritcu, editors, Certified Programs and Proofs (CPP) 2020, pages 367-381. ACM, 2020. URL: https://doi.org/10.1145/3372885.3373824.
  21. Magnus O. Myreen, Konrad Slind, and Michael J. C. Gordon. Extensible proof-producing compilation. In Oege de Moor and Michael I. Schwartzbach, editors, Compiler Construction (CC) 2009, pages 2-16. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-00722-4_2.
  22. Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, Cédric Fournet, Natalia Kulatova, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, and Santiago Zanella Béguelin. Evercrypt: A fast, verified, cross-platform cryptographic provider. In IEEE Symposium on Security and Privacy (SP) 2020, pages 983-1002. IEEE, 2020. URL: https://doi.org/10.1109/SP40000.2020.00114.
  23. Peter Schwabe, Benoît Viguier, Timmy Weerwag, and Freek Wiedijk. A Coq proof of the correctness of X25519 in TweetNaCl. In Computer Security Foundations Symposium (CSF) 2021, pages 1-16. IEEE, 2021. URL: https://doi.org/10.1109/CSF51468.2021.00023.
  24. Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, and Jean Yang. Secure distributed programming with value-dependent types. J. Funct. Program., 23(4):402-451, 2013. URL: https://doi.org/10.1017/S0956796813000142.
  25. Laurent Théry. Proving the group law for elliptic curves formally. Technical Report RT-0330, INRIA, 2007. URL: https://hal.inria.fr/inria-00129237.
  26. Jean Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, and Benjamin Beurdouche. HACL*: A verified modern cryptographic library. In Bhavani Thuraisingham, David Evans, Tal Malkin, and Dongyan Xu, editors, Conference on Computer and Communications Security (CCS) 2017, pages 1789-1806. ACM, 2017. URL: https://doi.org/10.1145/3133956.3134043.
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 About DROPS Imprint Privacy Contact