Generation of the weakest preconditions of programs with dynamic memory in symbolic execution

Misonizhnik A.V., Kostyukov Yu.O., Kostitsyn M.P., Mordvinov D.A., Koznov D.V. Generation of the weakest preconditions of programs with dynamic memory in symbolic execution. Scientific and Technical Journal of Information Technologies, Mechanics and Optics, 2022, vol. 22, no. 5, pp. 982–991 (in Russian). doi: 10.17586/2226-1494-2022-22-5-982-991

Symbolic execution is a widely used method for the systematic study of program execution paths; it allows solving a number of important problems related to verification of correctness: searching for errors and vulnerabilities, automatic test generation, etc. The main idea of symbolic execution is generation and use of symbolic expressions in the program analysis in direct order, i.e., from the entry point to the points of interest. At the same time, since the time of E.W. Dijkstra, the method of backward symbolic execution has been popular when the conditions for hitting the point of interest are extended to the entry point of the program due to the iterative calculation of the weakest preconditions. This method is usually much more difficult to implement than direct symbolic execution, so even the artifacts of the latter cannot be used in the implementation. In this paper, the relationship between direct and backward symbolic execution based on the calculation of the weakest preconditions is investigated. In particular, it is shown that the latter can be implemented using the former. A formal presentation of symbolic execution with lazy initialization for programs with dynamic memory is given. An algorithm for calculating the weakest preconditions for arbitrary symbolic executed program branches is proposed. The lazy initialization mechanism and the algorithm for calculating the weakest preconditions are implemented in KLEE, a symbolic virtual machine for the well-known LLVM platform. The proposed method allows performing backward symbolic analysis using direct symbolic execution. This is important for the implementation of bidirectional program execution which can be used both for program verification and for automatic test generation.

1. Baldoni R., Coppa E., D'Elia D.C., Demetrescu C., Finocchi I. A survey of symbolic execution techniques. ACM Computing Surveys, 2018, vol. 51, no. 3. https://doi.org/10.1145/3182657
2. Cadar C., Dunbar D., Engler D. KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. Proc. of the 8^th USENIX Conference on Operating Systems Design and Implementation, 2008, pp. 209–224.
3. Wang F., Shoshitaishvili Y. ANGR – the next generation of binary analysis.Proc. of the IEEE Cybersecurity Development (SecDev), 2017, pp. 8–9. https://doi.org/10.1109/SecDev.2017.14
4. Burnim J., Sen K. Heuristics for scalable dynamic test generation. Proc. of the ASE 2008 - 23^rd IEEE/ACM International Conference on Automated Software Engineering, 2008, pp. 443–446. https://doi.org/10.1109/ASE.2008.69
5. Tillmann N., Halleux J. Pex-white box test generation for .NET. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2008, vol. 4966, pp. 134–153. https://doi.org/10.1007/978-3-540-79124-9_10
6. Pǎsǎreanu C.S., Rungta N. Symbolic PathFinder: symbolic execution of Java bytecode. Proc. of the 25^th IEEE/ACM International Conference on Automated Software Engineering, 2010, pp. 179–180. https://doi.org/10.1145/1858996.1859035
7. Mossberg M., Manzano F., Hennenfent E., Groce A., Grieco G., Feist J., Brunson T., Dinaburg A. Manticore: A user-friendly symbolic execution framework for binaries and smart contracts. Proc. of the 34^th IEEE/ACM International Conference on Automated Software Engineering (ASE), 2019, pp. 1186–1189. https://doi.org/10.1109/ASE.2019.00133
8. Godefroid P., Klarlund N., Sen K. DART: Directed automated random testing. Proc. of the 2005 ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI), 2005, pp. 213–223.
9. Godefroid P., Levin M.Y., Molnar D. SAGE: whitebox fuzzing for security testing. Communications of the ACM, 2012, vol. 55, no. 3, pp. 40–44. https://doi.org/10.1145/2093548.2093564
10. Chipounov V., Kuznetsov V., Candea G. S2E: a platform for in-vivo multi-path analysis of software systems. ACM SIGPLAN Notices, 2011, vol. 46, no. 3, pp. 265–278. https://doi.org/10.1145/1961296.1950396
11. Vishnyakov A., Fedotov A., Kuts D., Novikov A., Parygina D., Kobrin E., Logunova V., Belecky P., Kurmangaleev S. Sydr: Cutting edge dynamic symbolic execution. Proc. of the 2020 Ivannikov Ispras Open Conference (ISPRAS), 2020, pp. 46–54. https://doi.org/10.1109/ISPRAS51486.2020.00014
12. Dinges P., Agha G. Targeted test input generation using symbolic-concrete backward execution. Proc. of the 29^th ACM/IEEE International Conference on Automated Software Engineering, 2014, pp. 31–36. https://doi.org/10.1145/2642937.2642951
13. Chandra S., Fink S.J., Sridharan M. Snugglebug: a powerful approach to weakest preconditions. ACM SIGPLAN Notices, 2009, vol. 44, no. 6, pp. 363–374. https://doi.org/10.1145/1543135.1542517
14. Dijkstra E.W. A Discipline of Programming. Englewood Cliffs, N.J., Prentice-Hall, 1976, XVII, 217 p.
15. Khurshid S., Pǎsǎreanu C.S., Visser W. Generalized symbolic execution for model checking and testing. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2003, pp. 553–568. https://doi.org/10.1007/3-540-36577-X_40
16. Anand S., Pǎsǎreanu C.S., Visser W. Symbolic execution with abstraction. International Journal on Software Tools for Technology Transfer, 2009, vol. 11, no. 1, pp. 53–67. https://doi.org/10.1007/s10009-008-0090-1
17. Lin Y. Symbolic execution with over-approximation.Ph.D. Thesis. The University of Melbourne, 2017.
18. Rungta N., Mercer E.G., Visser W. Efficient testing of concurrent programs with abstraction-guided symbolic execution. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2009, vol. 5578, pp. 174–191. https://doi.org/10.1007/978-3-642-02652-2_16
19. Berdine J., Calcagno C., O'Hearn P.W. Symbolic execution with separation logic. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2005, vol. 3780, pp. 52–68. https://doi.org/10.1007/11575467_5
20. Yi Q., Yang Z., Guo S., Wang C., Liu J., Zhao C. Postconditioned symbolic execution. Proc. of the 8^th IEEE International Conference on Software Testing, Verification and Validation (ICST), 2015, pp. 1–10. https://doi.org/10.1109/ICST.2015.7102601
21. McMillan K.L. Lazy annotation for program testing and verification. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2010, vol. 6174, pp. 104–118. https://doi.org/10.1007/978-3-642-14295-6_10
22. Deng X., Lee J., Robby. Efficient and formal generalized symbolic execution. Automated Software Engineering, 2012, vol. 19, no. 3, pp. 233–301. https://doi.org/10.1007/s10515-011-0089-9
23. Hoare C.A.R. An axiomatic basis for computer programming. Communications of the ACM, 1969, vol. 12, no. 10, pp. 576–580. https://doi.org/10.1145/363235.363259
24. Nepomniaschy V.A., Anureev I.S., Promskii A.V. Towards verification of C programs: axiomatic semantics of the C-kernel language. Programming and Computer Software, 2003, vol. 29, no. 6, pp. 338–350. https://doi.org/10.1023/B:PACS.0000004134.24714.e5
25. Blazy S., Leroy X. Mechanized semantics for the Clight subset of the C language. Journal of Automated Reasoning, 2009, vol. 43, no. 3, pp. 263–288. https://doi.org/10.1007/s10817-009-9148-3
26. De Moura L., Bjørner N. Z3: an efficient SMT solver. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2008, vol. 4963, pp. 337–340. https://doi.org/10.1007/978-3-540-78800-3_24
27. Ball T., Daniel J. Deconstructing dynamic symbolic execution. Proc. of the 2014 Marktoberdorf Summer School on Dependable Software Systems Engineering. IOS Press, 2015.

This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License