“Symcrete” memory Model with Lazy Initialization and Objects of Symbolic Sizes in KLEE
Sergey Antonovich MOROZOV,
Aleksandr Vladimirovich MISONIZHNIK,
Dmitry Aleksandrovich MORDVINOV,
Dmitry Arkadevich IVANOV https://doi.org/10.15514/ISPRAS-2023-35(3)-7
Abstract
Dynamic symbolic execution is a well-known technique for testing applications. It introduces symbolic variables – program data with no concrete value at the moment of instantiation – and uses them to systematically explore the execution paths in a program under analysis. However, not every value can be easily modelled as symbolic: for instance, some values may take values from restricted domains or have complex invariants, hard enough to model using existing logic theories, despite it is not a problem for concrete computations. In this paper, we propose an implementation of infrastructure for dealing with such “hard-to-be-modelled” values. We take the approach known as symcrete execution and implement its robust and scalable version in the well-known KLEE symbolic execution engine. We use this infrastructure to support the symbolic execution of LLVM programs with complex input data structures and input buffers with indeterminate sizes.
Keywords
Supporting agencies: This work is supported by the grant of the Russian Science Foundation (RSF) № 22-21-00697.
About the Authors
Sergey Antonovich MOROZOV
National Research University ‘Higher School of Economics’
Russian Federation
Russian Federation
Third-year student of Higher School of Economics
Aleksandr Vladimirovich MISONIZHNIK
IT Solutions Inc.
Russian Federation
Russian Federation
Senior software engineer
Dmitry Aleksandrovich MORDVINOV
St. Petersburg State University
Russian Federation
Russian Federation
PhD in Physics and Mathematics, Associate Professor at the Department of System Programming of St. Petersburg State University
Dmitry Arkadevich IVANOV
Huawei Technologies Co., Ltd.
Russian Federation
Russian Federation
Director of R&D Toolchain department
References
1. Cristian Cadar and Koushik Sen. “Symbolic execution for software testing: three decades later”. In: Communications of the ACM 56.2 (2013), pp. 82–90.
2. Clark Barrett and Cesare Tinelli. “Satisfiability modulo theories”. In: Handbook of model checking. Springer, 2018, pp. 305–343.
3. Leonardo de Moura and Nikolaj Bjørner. “Z3: An efficient SMT solver”. In: International conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer. 2008, pp. 337–340.
4. Haniel Barbosa et al. “cvc5: A versatile and industrial-strength SMT solver”. In: Tools and Algorithms for the Construction and Analysis of Systems: 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022, Proceedings, Part I. Springer. 2022, pp. 415–442.
5. Aina Niemetz and Mathias Preiner. “Bitwuzla at the SMT-COMP 2020”. In: arXiv preprint arXiv:2006.01621 (2020).
6. Corina S Pa˘sa˘reanu, Neha Rungta, and Willem Visser. “Symbolic execution with mixed concrete-symbolic solving”. In: Proceedings of the 2011 International Symposium on Software Testing and Analysis. 2011, pp. 34–44.
7. Awanish Pandey, Phani Raj Goutham Kotcharlakota, and Subhajit Roy. “Deferred concretization in symbolic execution via fuzzing”. In: Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis. 2019, pp. 228–238.
8. Misonijnik A. et al. “Automated testing of LLVM programs with complex input data structures”. In: Proceedings of ISP RAS 34.4 (2022), pp. 49–62.
9. Sarfraz Khurshid, Corina S Pa˘sa˘reanu, and Willem Visser. “Generalized symbolic execution for model checking and testing”. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer. 2003, pp. 553–568.
10. Cristian Cadar and Daniel Dunbar. KLEE. Version 2.3. 2022. URL: https://github.com/klee/klee/tree/v2.3.
11. Dirk Beyer. “Advances in Automatic Software Testing: Test-Comp 2022.” In: FASE. 2022, pp. 321–335.
12. Leonardo de Moura and Nikolaj Bjørner. Z3 4.12.1. Version 4.12.1. 2023. URL: https://github.com/Z3Prover/ z3/releases/tag/z3-4.12.1.
13. Brian Gough and Richard M Stallman. “An Introduction to GCC for the GNU Compilers gcc and g++”. In: Network Theory Ltd 258 (2004).
14. Peter Dinges and Gul Agha. “Targeted test input generation using symbolic-concrete backward execution”. In: Proceedings of the 29th ACM/IEEE international conference on Automated software engineering. 2014, pp. 31–36.
15. Koushik Sen, Darko Marinov, and Gul Agha. “CUTE: A concolic unit testing engine for C”. In: ACM SIGSOFT Software Engineering Notes 30.5 (2005), pp. 263–272.
16. David Trabish, Shachar Itzhaky, and Noam Rinetzky. “A bounded symbolic-size model for symbolic execution”. In: Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering. 2021, pp. 1190–1201.
17. Michael Sima´ˇcek. “Symbolic-size memory allocation support for Klee”. PhD thesis. Masarykova univerzita, Fakulta informatiky, 2018.
Review
For citations:
MOROZOV S.A., MISONIZHNIK A.V., MORDVINOV D.A., IVANOV D.A. “Symcrete” memory Model with Lazy Initialization and Objects of Symbolic Sizes in KLEE. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2023;35(3):91-108. https://doi.org/10.15514/ISPRAS-2023-35(3)-7
Email this article 