Document Open Access Logo

A Dynamic Logic for Symbolic Execution for the Smart Contract Programming Language Michelson

Authors Barnabas Arvay , Thi Thu Ha Doan , Peter Thiemann

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2024.3.pdf
  • Filesize: 1.26 MB
  • 26 pages

Document Identifiers

Author Details

Barnabas Arvay
  • University of Freiburg, Germany
Thi Thu Ha Doan
  • University of Freiburg, Germany
Peter Thiemann
  • University of Freiburg, Germany

Funding

  • Doan, Thi Thu Ha: Supported by the Tezos Foundation, grant COOC.

Cite As Get BibTex

Barnabas Arvay, Thi Thu Ha Doan, and Peter Thiemann. A Dynamic Logic for Symbolic Execution for the Smart Contract Programming Language Michelson. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 3:1-3:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.ECOOP.2024.3

Abstract

Verification of smart contracts is an important topic in the context of blockchain technology. We study an approach to verification that is based on symbolic execution. 
As a formal basis for symbolic execution, we design a dynamic logic for Michelson, the smart contract language of the Tezos blockchain, and prove its soundness in the proof assistant Agda. Towards the soundness proof we formalize the concrete semantics as well as its symbolic counterpart in a unified setting. The logic encompasses single contract runs as well as inter-contract runs chained in a single transaction.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Automated static analysis
Keywords
  • Smart Contract
  • Blockchain
  • Formal Verification
  • Symbolic Execution

Metrics

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

Supplementary Materials

References

  1. Wolfgang Ahrendt and Richard Bubel. Functional verification of smart contracts via strong data integrity. In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of Formal Methods, Verification and Validation: Applications, pages 9-24, Cham, 2020. Springer International Publishing. Google Scholar
  2. Elvira Albert, Miguel Gómez-Zamalloa, Laurent Hubert, and Germán Puebla. Verification of java bytecode using analysis and transformation of logic programs. In Michael Hanus, editor, Practical Aspects of Declarative Languages, pages 124-139, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. Google Scholar
  3. 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), pages 66-77, January 2018. URL: https://doi.org/10.1145/3167084.
  4. Permenev Anton, Dimitrov Dimitar, Tsankov Petar, Dana Drachsler-Cohen, and Martin Vechev. Verx: Safety verification of smart contracts. In 2020 IEEE Symposium on Security and Privacy (SP), pages 1661-1677, 2020. URL: https://doi.org/10.1109/SP40000.2020.00024.
  5. Luís Pedro Arrojado da Horta, João Santos Reis, Simão Melo de Sousa, and Mário Pereira. A tool for proving michelson smart contracts in why3. In 2020 IEEE International Conference on Blockchain (Blockchain), pages 409-414, 2020. URL: https://doi.org/10.1109/Blockchain50366.2020.00059.
  6. Barnabas Arvay, Thi Thu Ha Doan, and Peter Thiemann. Contract Orchestration for Michelson. Software, version 0.5 (visited on 2024-08-29). URL: https://freidok.uni-freiburg.de/data/255176.
  7. Daniel Balasubramanian, Zhenkai Zhang, Dan McDermet, and Gabor Karsai. Dynamic symbolic execution for the analysis of web server applications in java. In Proceedings of the 34th ACM/SIGAPP Symposium on Applied Computing, SAC '19, pages 2178-2185, New York, NY, USA, 2019. Association for Computing Machinery. URL: https://doi.org/10.1145/3297280.3297494.
  8. Guillaume Bau, Antoine Miné, Vincent Botbol, and Mehdi Bouaziz. Abstract interpretation of michelson smart-contracts. In Proceedings of the 11th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis, SOAP 2022, pages 36-43, New York, NY, USA, 2022. Association for Computing Machinery. URL: https://doi.org/10.1145/3520313.3534660.
  9. Bernhard Beckert, Vladimir Klebanov, and Benjamin Weiß. Dynamic logic for java. In Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Peter H. Schmitt, and Mattias Ulbrich, editors, Deductive Software Verification - The KeY Book: From Theory to Practice, pages 49-106. Springer International Publishing, Cham, 2016. URL: https://doi.org/10.1007/978-3-319-49812-6_3.
  10. B. Bernardo, R. Cauderlier, Z. Hu, B. Pesin, and J. Tesson. Mi-Cho-Coq, a framework for certifying Tezos smart contracts. In 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.
  11. Rod M. Burstall. Program proving as hand simulation with a little induction. In Jack L. Rosenfeld, editor, Information Processing, Proceedings of the 6th IFIP Congress 1974, Stockholm, Sweden, August 5-10, 1974, pages 308-312. North-Holland, 1974. Google Scholar
  12. Cristian Cadar, Daniel Dunbar, and Dawson R. Engler. KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In Richard Draves and Robbert van Renesse, editors, 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, December 8-10, 2008, San Diego, California, USA, Proceedings, pages 209-224. USENIX Association, 2008. URL: http://www.usenix.org/events/osdi08/tech/full_papers/cadar/cadar.pdf.
  13. Christoph Csallner, Nikolai Tillmann, and Yannis Smaragdakis. Dysy: dynamic symbolic execution for invariant inference. In Wilhelm Schäfer, Matthew B. Dwyer, and Volker Gruhn, editors, 30th International Conference on Software Engineering (ICSE 2008), Leipzig, Germany, May 10-18, 2008, pages 281-290. ACM, 2008. URL: https://doi.org/10.1145/1368088.1368127.
  14. L. Goodman. Tezos-a self-amending crypto-ledger, 2014. URL: https://www.tezos.com/static/papers/white-paper.pdf.
  15. Á. Hajdu and D. Jovanović. solc-verify: A modular verifier for solidity smart contracts. In S. Chakraborty and J. A. Navas, editors, Verified Software. Theories, Tools, and Experiments, pages 161-179. Springer International Publishing, 2020. Google Scholar
  16. David Harel, Jerzy Tiuryn, and Dexter Kozen. Dynamic Logic. MIT Press, Cambridge, MA, USA, 2000. Google Scholar
  17. Maritta Heisel, Wolfgang Reif, and Werner Stephan. Program verification by symbolic execution and induction. In Katharina Morik, editor, GWAI-87, 11th German Workshop on Artificial Intelligence, Geseke, Germany, September 28 - October 2, 1987, Proceedings, volume 152 of Informatik-Fachberichte, pages 201-210. Springer, 1987. URL: https://doi.org/10.1007/978-3-642-73005-4_22.
  18. Everett Hildenbrandt, Manasvi Saxena, Nishant Rodrigues, Xiaoran Zhu, Philip Daian, Dwight Guth, Brandon Moore, Daejun Park, Yi Zhang, Andrei Stefanescu, and Grigore Rosu. KEVM: A complete formal semantics of the Ethereum virtual machine. In 2018 IEEE 31st Computer Security Foundations Symposium (CSF), pages 204-217, 2018. URL: https://doi.org/10.1109/CSF.2018.00022.
  19. Y. Hirai. Defining the Ethereum virtual machine for interactive theorem provers. In Financial Cryptography and Data Security, pages 520-535. Springer International Publishing, 2017. Google Scholar
  20. James C. King. Symbolic execution and program testing. Commun. ACM, 19(7):385-394, 1976. URL: https://doi.org/10.1145/360248.360252.
  21. Daniel Lehmann and Michael Pradel. Wasabi: A framework for dynamically analyzing webassembly. In Proceedings of the Twenty-Fourth International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS '19, pages 1045-1058, New York, NY, USA, 2019. Association for Computing Machinery. URL: https://doi.org/10.1145/3297858.3304068.
  22. 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), pages 254-269, 2016. Google Scholar
  23. Séverine Maingaud, Vincent Balat, Richard Bubel, Reiner Hähnle, and Alexandre Miquel. Specifying imperative ML-like programs using dynamic logic. In Bernhard Beckert and Claude Marché, editors, Formal Verification of Object-Oriented Software - International Conference, FoVeOOS 2010, Paris, France, June 28-30, 2010, Revised Selected Papers, volume 6528 of Lecture Notes in Computer Science, pages 122-137. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-18070-5_9.
  24. Filipe Marques, José Fragoso Santos, Nuno Santos, and Pedro Adão. Concolic Execution for WebAssembly. In Karim Ali and Jan Vitek, editors, 36th European Conference on Object-Oriented Programming (ECOOP 2022), volume 222 of Leibniz International Proceedings in Informatics (LIPIcs), pages 11:1-11:29, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2022.11.
  25. Michelson: The language of smart contracts in Tezos. URL: https://tezos.gitlab.io/alpha/michelson.html.
  26. Mark Mossberg, Felipe Manzano, Eric Hennenfent, Alex Groce, Gustavo Grieco, Josselin Feist, Trent Brunson, and Artem Dinaburg. Manticore: A user-friendly symbolic execution framework for binaries and smart contracts. In 2019 34th IEEE/ACM International Conference on Automated Software Engineering (ASE), pages 1186-1189, 2019. URL: https://doi.org/10.1109/ASE.2019.00133.
  27. Yuki Nishida, Hiromasa Saito, Ran Chen, Akira Kawata, Jun Furuse, Kohei Suenaga, and Atsushi Igarashi. HELMHOLTZ: A verifier for Tezos smart contracts based on refinement types. New Generation Computing, 40:507-540, 2022. URL: https://doi.org/10.1007/s00354-022-00167-1.
  28. Nomadic Lab. Michelson: the language of smart contracts in tezos, 2018-2023. Last accessed 17 October 2023. URL: https://tezos.gitlab.io/michelson-reference/.
  29. 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), pages 912-915, October 2018. URL: https://doi.org/10.1145/3236024.3264591.
  30. Corina S. Pasareanu. Symbolic Execution: The Basics, pages 5-20. Springer International Publishing, Cham, 2020. URL: https://doi.org/10.1007/978-3-031-02551-8_2.
  31. Dominic Steinhöfel and Reiner Hähnle. Abstract execution. In Maurice H. ter Beek, Annabelle McIver, and José N. Oliveira, editors, Formal Methods - The Next 30 Years - Third World Congress, FM 2019, Porto, Portugal, October 7-11, 2019, Proceedings, volume 11800 of Lecture Notes in Computer Science, pages 319-336. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-30942-8_20.
  32. Petar Tsankov, Andrei Dan, Dana Drachsler-Cohen, Arthur Gervais, Florian Bünzli, and Martin Vechev. Securify: Practical security analysis of smart contracts. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, pages 67-82, October 2018. URL: https://doi.org/10.1145/3243734.3243780.
  33. Philip Wadler, Wen Kokke, and Jeremy G. Siek. Programming language foundations in Agda, August 2022. URL: https://plfa.inf.ed.ac.uk/22.08/.
  34. Conrad Watt, Petar Maksimović, Neelakantan R. Krishnaswami, and Philippa Gardner. A Program Logic for First-Order Encapsulated WebAssembly. In Alastair F. Donaldson, editor, 33rd European Conference on Object-Oriented Programming (ECOOP 2019), volume 134 of Leibniz International Proceedings in Informatics (LIPIcs), pages 9:1-9:30, Dagstuhl, Germany, 2019. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2019.9.
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