Генерация слабейших предусловий программ с динамической памятью в символьном исполнении

Мисонижник А.В., Костюков Ю.О., Костицын М.П., Мордвинов Д.А., Коз­нов Д.В. Генерация слабейших предусловий программ с динамической памятью в символьном исполнении // Научно-технический вестник информационных технологий, механики и оптики. 2022. Т. 22, № 5. С. 982–991. doi: 10.17586/2226-1494-2022-22-5-982-991

Предмет исследования. Символьное исполнение — широко известный метод систематического исследования путей исполнения программ. Метод позволяет решить ряд важных задач, связанных с контролем корректности: поиск ошибок и уязвимостей, автоматическая генерация тестов и др. Основная идея символьного исполнения — порождение и использование символьных логических выражений при анализе программ в прямом порядке, т. е. от входной точки к точкам интереса. Хорошо известен метод обратного символьного исполнения, когда условия попадания в точку интереса распространяются ко входной точке программы за счет итеративного вычисления слабейших предусловий. Реализовать этот метод, как правило, намного труднее, чем прямое символьное исполнение, так что даже артефакты последнего не удается использовать при реализации. Метод. Исследована связь между прямым и обратным символьными исполнениями на основе вычисления слабейших предусловий. В частности показано, как обратное исполнение может быть реализовано на базе прямого. Основные результаты. Приведено формальное описание процедуры символьного исполнения с ленивой инициализацией для программ с динамической памятью. Предложен алгоритм вычисления слабейших предусловий для произвольных ветвей исполнения программы. Механизм ленивой инициализации и алгоритм вычисления слабейших предусловий реализованы в символьной виртуальной машине KLEE, работающей на базе широко известной платформы LLVM. Практическая значимость. Представленный метод позволяет выполнять обратный символьный анализ при помощи прямого символьного исполнения. Это важно для реализации двунаправленного исполнения программ, которое может быть применено для верификации программ и автоматического порождения тестовых покрытий.

1. Baldoni R., Coppa E., D'Elia D.C., Demetrescu C., Finocchi I. A survey of symbolic execution techniques // ACM Computing Surveys. 2018. V. 51. N 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. P. 209–224.
3. Wang F., Shoshitaishvili Y. ANGR – the next generation of binary analysis // Proc. of the IEEE Cybersecurity Development (SecDev). 2017. P. 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. P. 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. V. 4966. P. 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. P. 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. P. 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. P. 213–223.
9. Godefroid P., Levin M.Y., Molnar D. SAGE: whitebox fuzzing for security testing // Communications of the ACM. 2012. V. 55. N 3. P. 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. V. 46. N 3. P. 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. P. 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. 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. V. 5578. P. 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. V. 3780. P. 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. P. 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. V. 6174. P. 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. V. 19. N 3. P. 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. V. 12. N 10. P. 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. V. 29. N 6. P. 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. V. 43. N 3. P. 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. V. 4963. P. 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