ntvНаучно-технический вестник информационных технологий, механики и оптикиScientific and Technical Journal of Information Technologies, Mechanics and Optics2226-14942500-0373Университет ИТМО10.17586/2226-1494-2022-22-5-982-991ntv-82Research ArticleКОМПЬЮТЕРНЫЕ СИСТЕМЫ И ИНФОРМАЦИОННЫЕ ТЕХНОЛОГИИCOMPUTER SCIENCEГенерация слабейших предусловий программ с динамической памятью в символьном исполненииGeneration of the weakest preconditions of programs with dynamic memory in symbolic executionhttps://orcid.org/0000-0002-5907-0324МисонижникА. В.MisonizhnikA. V.

Мисонижник Александр Владимирович — студент

Санкт-Петербург, 199034

sc 57203100912

 

Aleksandr V. Misonizhnik — Student

Saint Petersburg, 199034

sc 57203100912

misonijniki@gmail.comhttps://orcid.org/0000-0003-4607-039XКостюковЮ. О.KostyukovYu. O.

Костюков Юрий Олегович — аспирант

Санкт-Петербург, 199034

sc 57219623001

Yurii O. Kostyukov — PhD Student

Saint Petersburg, 199034

sc 57219623001

kostyukov.yurii@gmail.comhttps://orcid.org/0000-0001-9982-6571КостицынМ. П.KostitsynM. P.

Костицын Михаил Павлович — инженер-исследователь

Санкт-Петербург, 199034

Michael P. Kostitsyn — Research Engineer

Saint Petersburg, 199034

michael.kosticyn@gmail.comhttps://orcid.org/0000-0002-6437-3020МордвиновД. А.MordvinovD. A.

Мордвинов Дмитрий Александрович — кандидат физико-математических наук, доцент, доцент

Санкт-Петербург, 199034

sc 57199323753

Dmitry A. Mordvinov — PhD (Physics & Mathematics), Associate Professor, Associate Professor

Saint Petersburg, 199034

sc 57199323753

mordvinov.dmitry@gmail.comhttps://orcid.org/0000-0003-2632-3193КозновД. В.KoznovD. V.

Кознов Дмитрий Владимирович — доктор технических наук, доцент, профессор

Санкт-Петербург, 199034

sc 8885649400

Dmitry V. Koznov — D. Sc., Associate Professor, Professor

Saint Petersburg, 199034

sc 8885649400

d.koznov@spbu.ruСанкт-Петербургский государственный университетРоссияState University (SPbSU)Russian Federation202212122024225982991Copyright © Мисонижник А.В., Костюков Ю.О., Костицын М.П., Мордвинов Д.А., Кознов Д.В., 20242024Мисонижник А.В., Костюков Ю.О., Костицын М.П., Мордвинов Д.А., Кознов Д.В.Misonizhnik A.V., Kostyukov Y.O., Kostitsyn M.P., Mordvinov D.A., Koznov D.V.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://ntv.elpub.ru/jour/article/view/82Предмет исследования

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

Метод

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

Основные результаты

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

Практическая значимость

Практическая значимость. Представленный метод позволяет выполнять обратный символьный анализ при помощи прямого символьного исполнения. Это важно для реализации двунаправленного исполнения программ, которое может быть применено для верификации программ и автоматического порождения тестовых покрытий.

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.

слабейшие предусловиясимвольное исполнениеобратный символьный анализдвунаправленный анализавтоматическая генерация тестовweakest preconditionssymbolic executionbackward symbolic analysisbidirectional analysisautomatic test generationДанное исследование было поддержано грантом РНФ № 22-21-00697.The work is supported by the grant of RNF No. 22-21-00697.ReferencesBaldoni 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/3182657Baldoni 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/3182657Cadar 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.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.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.14Wang 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.14Burnim 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.69Burnim 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.69Tillmann 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_10Tillmann 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_10Pǎ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.1859035Pǎ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.1859035Mossberg 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.00133Mossberg 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.00133Godefroid 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.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.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.2093564Godefroid 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.2093564Chipounov 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.1950396Chipounov 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.1950396Vishnyakov 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.00014Vishnyakov 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.00014Dinges 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.2642951Dinges 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.2642951Chandra 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.1542517Chandra 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.1542517Dijkstra E.W. A Discipline of Programming. Englewood Cliffs, N.J.: Prentice-Hall, 1976. XVII, 217 p.Dijkstra E.W. A Discipline of Programming. Englewood Cliffs, N.J.: Prentice-Hall, 1976. XVII, 217 p.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_40Khurshid 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_40Anand 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-1Anand 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-1Lin Y. Symbolic execution with over-approximation: Ph.D. Thesis. The University of Melbourne, 2017.Lin Y. Symbolic execution with over-approximation. Ph.D. Thesis. The University of Melbourne, 2017.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_16Rungta 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_16Berdine 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_5Berdine 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_5Yi 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.7102601Yi 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.7102601McMillan 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_10McMillan 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_10Deng 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-9Deng 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-9Hoare 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.363259Hoare 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.363259Nepomniaschy 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.e5Nepomniaschy 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.e5Blazy 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-3Blazy 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-3De 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_24De 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_24Ball T., Daniel J. Deconstructing dynamic symbolic execution // Proc. of the 2014 Marktoberdorf Summer School on Dependable Software Systems Engineering. IOS Press, 2015.Ball T., Daniel J. Deconstructing dynamic symbolic execution. Proc. of the 2014 Marktoberdorf Summer School on Dependable Software Systems Engineering. IOS Press, 2015.

The authors declare that there are no conflicts of interest present.