Document Open Access Logo

Symbolic Execution Game Semantics

Authors Yu-Yang Lin, Nikos Tzevelekos

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2020.27.pdf
  • Filesize: 0.69 MB
  • 24 pages

Document Identifiers

Author Details

Yu-Yang Lin
  • Queen Mary University of London, UK
Nikos Tzevelekos
  • Queen Mary University of London, UK

Funding

Research funded by EPSRC (EP/P004172/1).

Acknowledgements

We would like to thank members of the K framework for their consistent support with K, and anonymous reviewers for their insightful reviews.

Cite AsGet BibTex

Yu-Yang Lin and Nikos Tzevelekos. Symbolic Execution Game Semantics. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 27:1-27:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.FSCD.2020.27

Abstract

We present a framework for symbolically executing and model checking higher-order programs with external (open) methods. We focus on the client-library paradigm and in particular we aim to check libraries with respect to any definable client. We combine traditional symbolic execution techniques with operational game semantics to build a symbolic execution semantics that captures arbitrary external behaviour. We prove the symbolic semantics to be sound and complete. This yields a bounded technique by imposing bounds on the depth of recursion and callbacks. We provide an implementation of our technique in the 𝕂 framework and showcase its performance on a custom benchmark based on higher-order coding errors such as reentrancy bugs.

Subject Classification

ACM Subject Classification
  • Theory of computation → Semantics and reasoning
Keywords
  • game semantics
  • symbolic execution
  • higher-order open programs

Metrics

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

Supplementary Materials

References

  1. S. Abramsky, D. R. Ghica, L. Ong, and A. Murawski. Algorithmic game semantics and component-based verification. In Proceedings of SAVBCS 2003: Specification and Verification of Component-Based Systems, Workshop at ESEC/FASE 2003, pages 66-74, 2003. published as Technical Report 03-11, Department of Computer Science, Iowa State University. URL: http://www.cs.iastate.edu/~leavens/SAVBCS/2003/papers/SAVCBS03.pdf.
  2. Samson Abramsky and Guy McCusker. Game semantics. In Ulrich Berger and Helmut Schwichtenberg, editors, Computational Logic, pages 1-55, Berlin, Heidelberg, 1999. Springer Berlin Heidelberg. Google Scholar
  3. Nicola Atzei, Massimo Bartoletti, and Tiziana Cimoli. A survey of attacks on ethereum smart contracts sok. In Proceedings of the 6th International Conference on Principles of Security and Trust - Volume 10204, pages 164-186, New York, NY, USA, 2017. Springer-Verlag New York, Inc. URL: https://doi.org/10.1007/978-3-662-54455-6_8.
  4. Cristian Cadar, Daniel Dunbar, and Dawson Engler. Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation, OSDI'08, pages 209-224, Berkeley, CA, USA, 2008. USENIX Association. URL: http://dl.acm.org/citation.cfm?id=1855741.1855756.
  5. Cristiano Calcagno, Dino Distefano, Jérémy Dubreil, Dominik Gabi, Pieter Hooimeijer, Martino Luca, Peter W. O'Hearn, Irene Papakonstantinou, Jim Purbrick, and Dulma Rodriguez. Moving fast with software verification. In Klaus Havelund, Gerard J. Holzmann, and Rajeev Joshi, editors, NASA Formal Methods - 7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings, volume 9058 of Lecture Notes in Computer Science, pages 3-11. Springer, 2015. Google Scholar
  6. Edmund M. Clarke, Daniel Kroening, and Flavio Lerda. A tool for checking ANSI-C programs. In Kurt Jensen and Andreas Podelski, editors, Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Proceedings, volume 2988 of Lecture Notes in Computer Science, pages 168-176. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-24730-2_15.
  7. Byron Cook, Kareem Khazem, Daniel Kroening, Serdar Tasiran, Michael Tautschnig, and Mark R. Tuttle. Model checking boot code from AWS data centers. In Hana Chockler and Georg Weissenbacher, editors, Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II, volume 10982 of Lecture Notes in Computer Science, pages 467-486. Springer, 2018. Google Scholar
  8. Agostino Cortesi and Matteo Zanioli. Widening and narrowing operators for abstract interpretation. Computer Languages, Systems & Structures, 37(1):24-42, 2011. URL: https://doi.org/10.1016/j.cl.2010.09.001.
  9. Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Robert M. Graham, Michael A. Harrison, and Ravi Sethi, editors, Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977, pages 238-252. ACM, 1977. URL: https://doi.org/10.1145/512950.512973.
  10. Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, and Xavier Rival. Why does astrée scale up? Formal Methods in System Design, 35(3):229-264, 2009. Google Scholar
  11. Aleksandar S. Dimovski. Program verification using symbolic game semantics. Theor. Comput. Sci., 560:364-379, 2014. URL: https://doi.org/10.1016/j.tcs.2014.01.016.
  12. Quinn Dupont. Experiments in Algorithmic Governance: A history and ethnography of "The DAO," a failed Decentralized Autonomous Organization, chapter 8, pages 157-177. Routledge, 2017. Google Scholar
  13. William E. Howden. Symbolic testing and the dissect symbolic evaluation system. Software Engineering, IEEE Transactions on, SE-3:266-278, August 1977. URL: https://doi.org/10.1109/TSE.1977.231144.
  14. Dan R. Ghica. Applications of game semantics: From program analysis to hardware synthesis. In Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009, 11-14 August 2009, Los Angeles, CA, USA, pages 17-26. IEEE Computer Society, 2009. URL: https://doi.org/10.1109/LICS.2009.26.
  15. Dan R. Ghica and Guy McCusker. Reasoning about idealized ALGOL using regular languages. In Ugo Montanari, José D. P. Rolim, and Emo Welzl, editors, Automata, Languages and Programming, 27th International Colloquium, ICALP 2000, Geneva, Switzerland, July 9-15, 2000, Proceedings, volume 1853 of Lecture Notes in Computer Science, pages 103-115. Springer, 2000. URL: https://doi.org/10.1007/3-540-45022-X_10.
  16. Dan R. Ghica and Nikos Tzevelekos. A system-level game semantics. Electr. Notes Theor. Comput. Sci., 286:191-211, 2012. URL: https://doi.org/10.1016/j.entcs.2012.08.013.
  17. Ilya Grishchenko, Matteo Maffei, and Clara Schneidewind. Foundations and tools for the static analysis of ethereum smart contracts. In Hana Chockler and Georg Weissenbacher, editors, Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I, volume 10981 of Lecture Notes in Computer Science, pages 51-78. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-96145-3_4.
  18. A. Jeffrey and J. Rathke. A fully abstract may testing semantics for concurrent objects. In Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, pages 101-112, July 2002. URL: https://doi.org/10.1109/LICS.2002.1029820.
  19. James C. King. A new approach to program testing. SIGPLAN Not., 10(6):228-233, April 1975. URL: https://doi.org/10.1145/390016.808444.
  20. Daniel Kroening. The CBMC homepage. http://www.cprover.org/cbmc/, 2017. [Online; accessed 13-Jun-2017]. URL: http://www.cprover.org/cbmc/.
  21. James Laird. A fully abstract trace semantics for general references. In Lars Arge, Christian Cachin, Tomasz Jurdzinski, and Andrzej Tarlecki, editors, Automata, Languages and Programming, 34th International Colloquium, ICALP 2007, Wroclaw, Poland, July 9-13, 2007, Proceedings, volume 4596 of Lecture Notes in Computer Science, pages 667-679. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-73420-8_58.
  22. C. Liu, H. Liu, Z. Cao, Z. Chen, B. Chen, and B. Roscoe. Reguard: Finding reentrancy bugs in smart contracts. In 2018 IEEE/ACM 40th International Conference on Software Engineering: Companion (ICSE-Companion), pages 65-68, May 2018. Google Scholar
  23. 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. ACM. URL: https://doi.org/10.1145/2976749.2978309.
  24. Andrzej S. Murawski, Steven J. Ramsay, and Nikos Tzevelekos. A contextual equivalence checker for IMJ*. In Bernd Finkbeiner, Geguang Pu, and Lijun Zhang, editors, Automated Technology for Verification and Analysis, pages 234-240, Cham, 2015. Springer International Publishing. Google Scholar
  25. Andrzej S. Murawski and Nikos Tzevelekos. Higher-order linearisability. In 28th International Conference on Concurrency Theory, CONCUR 2017, September 5-8, 2017, Berlin, Germany, pages 34:1-34:18, 2017. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2017.34.
  26. Phuc C. Nguyen, Thomas Gilray, Sam Tobin-Hochstadt, and David Van Horn. Soft contract verification for higher-order stateful programs. PACMPL, 2(POPL):51:1-51:30, 2018. URL: https://doi.org/10.1145/3158139.
  27. Phuc C. Nguyen and David Van Horn. Relatively complete counterexamples for higher-order programs. In David Grove and Steve Blackburn, editors, Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015, pages 446-456. ACM, 2015. URL: https://doi.org/10.1145/2737924.2737971.
  28. Ivica Nikolić, Aashish Kolluri, Ilya Sergey, Prateek Saxena, and Aquinas Hobor. Finding the greedy, prodigal, and suicidal contracts at scale. In Proceedings of the 34th Annual Computer Security Applications Conference, ACSAC '18, pages 653-663, New York, NY, USA, 2018. ACM. URL: https://doi.org/10.1145/3274694.3274743.
  29. Doron A. Peled. All from one, one for all: on model checking using representatives. In Costas Courcoubetis, editor, Computer Aided Verification, 5th International Conference, CAV '93, Elounda, Greece, June 28 - July 1, 1993, Proceedings, volume 697 of Lecture Notes in Computer Science, pages 409-423. Springer, 1993. URL: https://doi.org/10.1007/3-540-56922-7_34.
  30. Andrew Pitts and Ian Stark. Operational reasoning for functions with local state. In Higher Order Operational Techniques in Semantics, pages 227-273. Cambridge University Press, 1998. Google Scholar
  31. Andrew M. Pitts. Nominal Sets: Names and Symmetry in Computer Science. Cambridge University Press, New York, NY, USA, 2013. Google Scholar
  32. Grigore Roşu and Traian Şerbănuţă. An overview of the k semantic framework. The Journal of Logic and Algebraic Programming, 79:397–434, August 2010. URL: https://doi.org/10.1016/j.jlap.2010.03.012.
  33. Robert S. Boyer, Bernard Elspas, and Karl Levitt. Select—a formal system for testing and debugging programs by symbolic execution. ACM SIGPLAN Notices, 10:234-245, June 1975. URL: https://doi.org/10.1145/390016.808445.
  34. Ryosuke Sato and Naoki Kobayashi. Modular verification of higher-order functional programs. In Hongseok Yang, editor, Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, volume 10201 of Lecture Notes in Computer Science, pages 831-854. Springer, 2017. URL: https://doi.org/10.1007/978-3-662-54434-1_31.
  35. Ryosuke Sato, Hiroshi Unno, and Naoki Kobayashi. Towards a scalable software model checker for higher-order programs. In Elvira Albert and Shin-Cheng Mu, editors, Proceedings of the ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation, PEPM 2013, Rome, Italy, January 21-22, 2013, pages 53-62. ACM, 2013. URL: https://doi.org/10.1145/2426890.2426900.
  36. Koushik Sen and Gul Agha. Cute and jcute: Concolic unit testing and explicit path model-checking tools. In Thomas Ball and Robert B. Jones, editors, Computer Aided Verification, pages 419-423, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. Google Scholar
  37. Olin Shivers. Control-Flow Analysis of Higher-Order Languages. PhD thesis, Carnegie-Mellon University, 1991. Google Scholar
  38. Sam Tobin-Hochstadt and David Van Horn. Higher-order symbolic execution via contracts. In Gary T. Leavens and Matthew B. Dwyer, editors, Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2012, part of SPLASH 2012, Tucson, AZ, USA, October 21-25, 2012, pages 537-554. ACM, 2012. URL: https://doi.org/10.1145/2384616.2384655.
  39. Antti Valmari. Stubborn sets for reduced state space generation. In Grzegorz Rozenberg, editor, Advances in Petri Nets 1990 [10th International Conference on Applications and Theory of Petri Nets, Bonn, Germany, June 1989, Proceedings], volume 483 of Lecture Notes in Computer Science, pages 491-515. Springer, 1989. URL: https://doi.org/10.1007/3-540-53863-1_36.
  40. Insu Yun, Sangho Lee, Meng Xu, Yeongjin Jang, and Taesoo Kim. Qsym: A practical concolic execution engine tailored for hybrid fuzzing. In Proceedings of the 27th USENIX Conference on Security Symposium, SEC'18, pages 745-761, Berkeley, CA, USA, 2018. USENIX Association. URL: http://dl.acm.org/citation.cfm?id=3277203.3277260.
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