Document Open Access Logo

Toward Tool-Independent Summaries for Symbolic Execution

Authors Frederico Ramos , Nuno Sabino , Pedro Adão , David A. Naumann , José Fragoso Santos

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2023.24.pdf
  • Filesize: 1.2 MB
  • 29 pages

Document Identifiers

Author Details

Frederico Ramos
  • Instituto Superior Técnico, University of Lisbon, Portugal
  • INESC-ID Lisbon, Portugal
Nuno Sabino
  • Instituto Superior Técnico, University of Lisbon, Portugal
  • Carnegie Mellon University, Pittsburgh, PA, USA
  • Institute of Telecommunications, Campus de Santiago, Aveiro, Portugal
Pedro Adão
  • Instituto Superior Técnico, University of Lisbon, Portugal
  • Institute of Telecommunications, Campus de Santiago, Aveiro, Portugal
David A. Naumann
  • Stevens Institute of Technology, Hoboken, NJ, USA
José Fragoso Santos
  • Instituto Superior Técnico, University of Lisbon, Portugal
  • INESC-ID Lisbon, Portugal

Funding

The authors were supported by Fundação para a Ciência e a Tecnologia (UIDB/50008/2020, Instituto de Telecomunicações, and UIDB/50021/2020, INESC-ID multi-annual funding, and PhD grant SFRH/BD/150692/2020), project DIVINA (CMU/TIC/0053/2021), the SmartRetail project (C6632206063-00466847) financed by IAPMEI, the European Commission under grant agreement number 830892 (SPARTA), and the NSF award CNS-1718713.

Cite AsGet BibTex

Frederico Ramos, Nuno Sabino, Pedro Adão, David A. Naumann, and José Fragoso Santos. Toward Tool-Independent Summaries for Symbolic Execution. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 24:1-24:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ECOOP.2023.24

Abstract

We introduce a new symbolic reflection API for implementing tool-independent summaries for the symbolic execution of C programs. We formalise the proposed API as a symbolic semantics and extend two state-of-the-art symbolic execution tools with support for it. Using the proposed API, we implement 67 tool-independent symbolic summaries for a total of 26 libc functions. Furthermore, we present SumBoundVerify, a fully automatic summary validation tool for checking the bounded correctness of the symbolic summaries written using our symbolic reflection API. We use SumBoundVerify to validate 37 symbolic summaries taken from 3 state-of-the-art symbolic execution tools, angr, Binsec and Manticore, detecting a total of 24 buggy summaries.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Software verification and validation
  • Security and privacy → Formal methods and theory of security
Keywords
  • Symbolic Execution
  • Runtime Modelling
  • Symbolic Summaries

Metrics

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

Supplementary Materials

References

  1. Alessandro Abate, Cristina David, Pascal Kesseli, Daniel Kroening, and Elizabeth Polgreen. Counterexample guided inductive synthesis modulo theories. In Hana Chockler and Georg Weissenbacher, editors, Computer Aided Verification, pages 270-288, Cham, 2018. Springer International Publishing. Google Scholar
  2. Saswat Anand, Patrice Godefroid, and Nikolai Tillmann. Demand-driven compositional symbolic execution. In Tools and Algorithms for the Construction and Analysis of Systems, pages 367-381, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. Google Scholar
  3. Andrew Appel. The Verifiable C string library, 2021. Software distribution that accompanies [Andrew W. Appel et al., 2021]. URL: https://softwarefoundations.cis.upenn.edu/vc-current/index.html.
  4. Andrew W. Appel, Lennart Beringer, and Qinxiang Cao. Verifiable C, volume 5 of Software Foundations. Electronic textbook, 2021. URL: http://softwarefoundations.cis.upenn.edu.
  5. Krzysztof R. Apt. Ten Years of Hoare’s Logic: A Survey—Part I. ACM Trans. Program. Lang. Syst., 3(4):431-483, October 1981. URL: https://doi.org/10.1145/357146.357150.
  6. Roberto Baldoni, Emilaio Coppa, Daniele Cono D’elia, Camil Demetrescu, and Irene Finocchi. A survey of symbolic execution techniques. ACM Comput. Surv., 51(3), May 2018. URL: https://doi.org/10.1145/3182657.
  7. Thomas Ball, Byron Cook, Vladimir Levin, and Sriram K. Rajamani. Slam and static driver verifier: Technology transfer of formal methods inside microsoft. In Integrated Formal Methods, pages 1-20, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. Google Scholar
  8. Zuzana Baranová, Jiří Barnat, Katarína Kejstová, Tadeáš Kučera, Henrich Lauko, Jan Mrázek, Petr Ročkai, and Vladimír Štill. Model checking of C and C++ with DIVINE 4. In Automated Technology for Verification and Analysis, pages 201-207, Cham, 2017. Springer International Publishing. Google Scholar
  9. Clark W. Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, and Cesare Tinelli. CVC4. In Proceedings of the 23rd International Conference on Computer Aided Verification CAV 2011, volume 6806 of Lecture Notes in Computer Science, pages 171-177. Springer, 2011. Google Scholar
  10. Dirk Beyer. Software Verification: 10th Comparative Evaluation (SV-COMP 2021). In Tools and Algorithms for the Construction and Analysis of Systems, pages 401-422, Cham, 2021. Springer International Publishing. Google Scholar
  11. Dirk Beyer. Status Report on Software Testing: Test-Comp 2021. In Fundamental Approaches to Software Engineering, pages 341-357, Cham, 2021. Springer International Publishing. Google Scholar
  12. Dirk Beyer. Advances in Automatic Software Testing: Test-Comp 2022. In Fundamental Approaches to Software Engineering - 25th International Conference, FASE 2022, volume 13241 of Lecture Notes in Computer Science, pages 321-335. Springer, 2022. Google Scholar
  13. Dirk Beyer. Progress on software verification: SV-COMP 2022. In Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, volume 13244 of Lecture Notes in Computer Science, pages 375-402. Springer, 2022. Google Scholar
  14. Robert S. Boyer, Bernard Elspas, and Karl N. Levitt. SELECT—a Formal System for Testing and Debugging Programs by Symbolic Execution. SIGPLAN Not., 10(6):234-245, April 1975. URL: https://doi.org/10.1145/390016.808445.
  15. 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, USA, 2008. USENIX Association. Google Scholar
  16. Marek Chalupa, Vincent Mihalkovič, Anna Řechtáčková, Lukáš Zaoral, and Jan Strejček. Symbiotic 9: String analysis and backward symbolic execution with loop folding. In Tools and Algorithms for the Construction and Analysis of Systems, pages 462-467, Cham, 2022. Springer International Publishing. Google Scholar
  17. Vitaly Chipounov, Volodymyr Kuznetsov, and George Candea. The S2E Platform: Design, Implementation, and Applications. ACM Transactions on Computer Systems - TOCS, 30:1-49, February 2012. URL: https://doi.org/10.1145/2110356.2110358.
  18. L. Daniel, S. Bardin, and T. Rezk. Binsec/Rel: Efficient Relational Symbolic Execution for Constant-Time at Binary-Level. In 2020 IEEE Symposium on Security and Privacy (SP), pages 1021-1038, Los Alamitos, CA, USA, May 2020. IEEE Computer Society. URL: https://doi.org/10.1109/SP40000.2020.00074.
  19. R. David, S. Bardin, T. D. Ta, L. Mounier, J. Feist, M. Potet, and J. Marion. Binsec/se: A dynamic symbolic execution toolkit for binary-level analysis. In 2016 IEEE 23rd International Conference on Software Analysis, Evolution, and Reengineering (SANER), volume 1, pages 653-656, 2016. URL: https://doi.org/10.1109/SANER.2016.43.
  20. Leonardo de Moura and Nikolaj Bjørner. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems, pages 337-340, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. Google Scholar
  21. José Fragoso Santos, Petar Maksimović, Sacha-Élie Ayoun, and Philippa Gardner. Gillian, Part I: A multi-language platform for symbolic execution. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2020. Association for Computing Machinery, 2020. Google Scholar
  22. GNU. GNU libiberty, 2022. Accessed: 2023-06-19. URL: https://gcc.gnu.org/onlinedocs/libiberty/.
  23. GNU. The GNU C library, 2022. Accessed: 2023-06-19. URL: https://www.gnu.org/software/libc/.
  24. Patrice Godefroid. Compositional Dynamic Test Generation. SIGPLAN Not., 42(1):47-54, January 2007. URL: https://doi.org/10.1145/1190215.1190226.
  25. Patrice Godefroid, Shuvendu K. Lahiri, and Cindy Rubio-González. Statically validating must summaries for incremental compositional dynamic test generation. In Static Analysis - 18th International Symposium, SAS 2011, Venice, Italy, September 14-16, 2011. Proceedings, volume 6887 of Lecture Notes in Computer Science, pages 112-128. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-23702-7_12.
  26. Patrice Godefroid, Michael Y. Levin, and David A Molnar. Automated whitebox fuzz testing. In Network Distributed Security Symposium (NDSS). Internet Society, 2008. Google Scholar
  27. Patrice Godefroid and Daniel Luchaup. Automatic Partial Loop Summarization in Dynamic Test Generation. In Proceedings of the 2011 International Symposium on Software Testing and Analysis, ISSTA '11, pages 23-33, New York, NY, USA, 2011. Association for Computing Machinery. URL: https://doi.org/10.1145/2001420.2001424.
  28. Patrice Godefroid, Aditya V. Nori, Sriram K. Rajamani, and SaiDeep Tetali. Compositional may-must program analysis: unleashing the power of alternation. In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, pages 43-56. ACM, 2010. URL: https://doi.org/10.1145/1706299.1706307.
  29. Denis Gopan and Thomas Reps. Low-level library analysis and summarization. In Computer Aided Verification, pages 68-81, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. Google Scholar
  30. Samin S. Ishtiaq and Peter W. O'Hearn. BI as an assertion language for mutable data structures. In Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, London, UK, pages 14-26. ACM, 2001. URL: https://doi.org/10.1145/360204.375719.
  31. Joxan Jaffar, Rasool Maghareh, Sangharatna Godboley, and Xuan-Linh Ha. TracerX: Dynamic Symbolic Execution with Interpolation (Competition Contribution). In Fundamental Approaches to Software Engineering, pages 530-534, Cham, 2020. Springer International Publishing. Google Scholar
  32. Timotej Kapus, Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, and Cristian Cadar. Computing summaries of string loops in c for better testing and refactoring. In PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 874-888, New York, NY, USA, 2019. Association for Computing Machinery. Google Scholar
  33. Sarfraz Khurshid, Corina S. Pasareanu, and Willem Visser. Generalized symbolic execution for model checking and testing. In 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2003, volume 2619 of Lecture Notes in Computer Science. Springer, 2003. Google Scholar
  34. James C. King. A new approach to program testing. In Proceedings of the International Conference on Reliable Software, pages 228-233, New York, NY, USA, 1975. Association for Computing Machinery. URL: https://doi.org/10.1145/800027.808444.
  35. Yude Lin, Tim Miller, and Harald Søndergaard. Compositional symbolic execution using fine-grained summaries. In 2015 24th Australasian Software Engineering Conference, pages 213-222, 2015. URL: https://doi.org/10.1109/ASWEC.2015.32.
  36. Petar Maksimovic, Sacha-Élie Ayoun, José Fragoso Santos, and Philippa Gardner. Gillian, part II: real-world verification for javascript and C. In Computer Aided Verification - 33rd International Conference, CAV 2021, volume 12760 of Lecture Notes in Computer Science, pages 827-850. Springer, 2021. Google Scholar
  37. Petar Maksimovic, Caroline Cronjäger, Julian Sutherland, Andreas Lööw, Sacha-Élie Ayoun, and Philippa Gardner. Exact separation logic. CoRR, abs/2208.07200, 2022. URL: https://arxiv.org/abs/2208.07200.
  38. 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.
  39. Manh-Dung Nguyen, S'ebastien Bardin, Richard Bonichon, R. Groz, and Matthieu Lemerre. Binary-level directed fuzzing for use-after-free vulnerabilities. ArXiv, abs/2002.10751, 2020. URL: https://arxiv.org/abs/2002.10751.
  40. Peter O'Hearn. Incorrectness logic. Proceedings of the ACM on Programming Languages, 4:1-32, December 2019. URL: https://doi.org/10.1145/3371078.
  41. Nadia Polikarpova and Ilya Sergey. Structuring the synthesis of heap-manipulating programs. Proc. ACM Program. Lang., 3(POPL):72:1-72:30, 2019. Google Scholar
  42. Rui Qiu, Guowei Yang, Corina S. Pasareanu, and Sarfraz Khurshid. Compositional symbolic execution with memoized replay. In 2015 IEEE/ACM 37th IEEE International Conference on Software Engineering, volume 1, pages 632-642, 2015. URL: https://doi.org/10.1109/ICSE.2015.79.
  43. E. Reisner, C. Song, K. Ma, J. S. Foster, and A. Porter. Using symbolic evaluation to understand behavior in configurable software systems. In 2010 ACM/IEEE 32nd International Conference on Software Engineering, volume 1, pages 445-454, 2010. URL: https://doi.org/10.1145/1806799.1806864.
  44. John C. Reynolds. Separation logic: A logic for shared mutable data structures. In 17th IEEE Symposium on Logic in Computer Science LICS 2002, pages 55-74. IEEE Computer Society, 2002. Google Scholar
  45. Nuno Sabino. Automatic vulnerability detection: Using compressed execution traces to guide symbolic execution. Master’s thesis, Instituto Superior Técnico, November 2019. Google Scholar
  46. Salvatore Sanfilippo. Simple dynamic strings, 2015. Accessed: 2023-06-19. URL: https://github.com/antirez/sds.
  47. José Fragoso Santos, Petar Maksimovic, Théotime Grohens, Julian Dolby, and Philippa Gardner. Symbolic Execution for JavaScript. In Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018, Frankfurt am Main, Germany, September 03-05, 2018, pages 11:1-11:14. ACM, 2018. Google Scholar
  48. José Fragoso Santos, Petar Maksimovic, Gabriela Sampaio, and Philippa Gardner. JaVerT 2.0: compositional symbolic execution for JavaScript. Proc. ACM Program. Lang., 3(POPL):66:1-66:31, 2019. Google Scholar
  49. Vaibhav Sharma, Kesha Hietala, and Stephen McCamant. Finding substitutable binary code by synthesizing adapters. IEEE Transactions on Software Engineering, PP:1-1, July 2019. URL: https://doi.org/10.1109/TSE.2019.2931000.
  50. Y. Shoshitaishvili, R. Wang, C. Salls, N. Stephens, M. Polino, A. Dutcher, J. Grosen, S. Feng, C. Hauser, C. Kruegel, and G. Vigna. SOK: (State of) The Art of War: Offensive Techniques in Binary Analysis. In 2016 IEEE Symposium on Security and Privacy (SP), pages 138-157, 2016. URL: https://doi.org/10.1109/SP.2016.17.
  51. Jan Strejček and Marek Trtík. Abstracting Path Conditions. In Proceedings of the 2012 International Symposium on Software Testing and Analysis, ISSTA 2012, pages 155-165, New York, NY, USA, 2012. Association for Computing Machinery. URL: https://doi.org/10.1145/2338965.2336772.
  52. Emina Torlak and Rastislav Bodik. Growing solver-aided languages with rosette. In Proceedings of the 2013 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming & Software, Onward! 2013, pages 135-152, New York, NY, USA, 2013. Association for Computing Machinery. URL: https://doi.org/10.1145/2509578.2509586.
  53. Verifiable C - Verif_strlib. Bug in strcmp function. Accessed: 2023-06-19. URL: https://softwarefoundations.cis.upenn.edu/vc-current/Verif_strlib.html.
  54. Willem Visser, Klaus Havelund, Guillaume Brat, Seungjoon Park, and Flavio Lerda. Model checking programs. Autom. Softw. Eng., 10:203-232, April 2003. URL: https://doi.org/10.1023/A:1022920129859.
  55. Richard Wiedenhöft. C Hash map, 2014. Accessed: 2023-06-19. URL: https://gist.github.com/Richard-W/9568649.
  56. Greta Yorsh, Eran Yahav, and Satish Chandra. Generating precise and concise procedure summaries. In Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, pages 221-234. ACM, 2008. Google Scholar
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