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

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

Метод. Исследована связь между прямым и обратным символьными исполнениями на основе вычисления слабейших предусловий. В частности показано, как обратное исполнение может быть реализовано на базе прямого.

Основные результаты. Приведено формальное описание процедуры символьного исполнения с ленивой инициализацией для программ с динамической памятью. Предложен алгоритм вычисления слабейших предусловий для произвольных ветвей исполнения программы. Механизм ленивой инициализации и алгоритм вычисления слабейших предусловий реализованы в символьной виртуальной машине 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 8th 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 — 23rd 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 25th 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 34th 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, 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), 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. 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 8th 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.