doi: 10.17586/2226-1494-2022-22-5-982-991


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

A. V. Misonizhnik, Y. . Kostyukov, M. P. Kostitsyn, D. A. Mordvinov, D. V. Koznov


Read the full article  ';
Article in Russian

For citation:
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


Abstract
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.

Keywords: weakest preconditions, symbolic execution, backward symbolic analysis, bidirectional analysis, automatic test generation

Acknowledgements. The work is supported by the grant of RNF No. 22-21-00697.

References
  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
  12. Dinges P., Agha G. Targeted test input generation using symbolic-concrete backward execution. Proc. of the 29th 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 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.


Creative Commons License

This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License
Copyright 2001-2024 ©
Scientific and Technical Journal
of Information Technologies, Mechanics and Optics.
All rights reserved.

Яндекс.Метрика