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

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 8th 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 — 23rd 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 25th 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 34th 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 Ispras Open Conference (ISPRAS). 2020. P. 46–54. https://doi.org/10.1109/ISPRAS51486.2020.00014

12. Dinges P., Agha G. Targeted test input generation using symbolicconcrete backward execution // Proc. of the 29th ACM/IEEE International Conference on Automated Software Engineering. 2014. P. 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. V. 44. N 6. P. 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. P. 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. V. 11. N 1. P. 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 8th 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.