Automatic verification of heap-manipulating programs
https://doi.org/10.15514/ISPRAS-2019-31(5)-3
Abstract
Theoretical foundations of compositional reasoning about heaps in imperative programming languages are investigated. We introduce a novel concept of compositional symbolic memory and its relevant properties. We utilize these formal foundations to build up a compositional algorithm that generates generalized heaps, terms of symbolic heap calculus, which characterize arbitrary cyclic code segments. All states inferred by this calculus precisely correspond to reachable states of the original program. We establish the correspondence between inference in this calculus and execution of pure second-order functional programs. The contribution of this work is as follows: (1) a formal model of compositional symbolic memory is proposed; (2) the properties of its correctness are formulated; (3) the calculus of symbolic heaps has been introduced: the conclusions in this calculus give all attainable states of the program; (4) the concept of generalized heaps is introduced, an algorithm for automatic modular construction of generalized heaps according to an imperative program is proposed; (5) an approach is proposed to reduce the problem of finding an output in calculus of symbolic heaps to the problem of proving the safety of functional programs.
About the Authors
Yurii Kostyukov
Saint Petersburg State University
Russian Federation
Received the bachelor’s degree in information technology from Saint Petersburg State University in 2019
Russian Federation
Received the bachelor’s degree in information technology from Saint Petersburg State University in 2019
Konstantin Batoev
Saint Petersburg State University
Russian Federation
Received the bachelor’s degree in information technology from Saint Petersburg State University in 2019
Russian Federation
Received the bachelor’s degree in information technology from Saint Petersburg State University in 2019
Dmitry Mordvinov
Saint Petersburg State University,
JetBrains Research
Russian Federation
Senior lecturer in Saint Petersburg State University, currently pursuing the Ph.D. degree in information technology
Russian Federation
Senior lecturer in Saint Petersburg State University, currently pursuing the Ph.D. degree in information technology
Michael Kostitsyn
Saint Petersburg State University
Russian Federation
Received the bachelor’s degree in information technology from Saint Petersburg State University in 2019
Russian Federation
Received the bachelor’s degree in information technology from Saint Petersburg State University in 2019
Aleksandr Misonizhnik
Saint Petersburg State University
Russian Federation
Received the bachelor’s degree in information technology from Saint Petersburg State University in 2018
Russian Federation
Received the bachelor’s degree in information technology from Saint Petersburg State University in 2018
References
1. Distefano D. Attacking large industrial code with bi-abductive inference. Lecture Notes in Computer Science, vol. 5825, 2009, pp. 1–8.
2. Calcagno C. et al. Compositional shape analysis by means of bi-abduction. Journal of the ACM, vol. 58, no. 6, 2011, p. 26:1-26:66.
3. Gurfinkel A. et al. The SeaHorn verification framework. Lecture Notes in Computer Science, vol. 9206, 2015, pp. 343–361.
4. Anand S., Godefroid P., and Tillmann N. Demand-driven compositional symbolic execution. Lecture Notes in Computer Science, vol. 4963, 2008, pp. 367–381.
5. Distefano D. and Parkinson J M. J. jStar: Towards practical verification for Java. ACM Sigplan Notices, vol. 43, issue 10, 2008, pp. 213– 226.
6. Calcagno C. and Distefano D. Infer: An automatic program verifier for memory safety of C programs. Lecture Notes in Computer Science, vol. 6617, 2011, pp. 459–465.
7. Tillmann N. and De Halleux J. Pex–white box test generation for. net. Lecture Notes in Computer Science, vol. 4966, 2008, pp. 134– 153.
8. Cousot P. and Cousot R. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, 1977, pp. 238– 252.
9. Khurshid S., Păsăreanu C. S., and Visser W. Generalized Symbolic Execution for Model Checking and Testing. Lecture Notes in Computer Science, vol. 2619, 2003, pp. 553–568.
10. Vazou N., Bakst A., and Jhala R. Bounded refinement types. ACM SIGPLAN Notices, vol. 50, issue 9, 2015, pp. 48–61.
11. Godefroid P. Compositional Dynamic Test Generation. ACM SIGPLAN Notices, vol. 42, issue 1, 2007, pp. 47–54.
12. Biere A. et al. Symbolic Model Checking without BDDs. Lecture Notes in Computer Science, vol. 1579, 1999, pp. 193–207.
13. Deng X., Lee J. et al. Efficient and Formal Generalized Symbolic Execution. Automated Software Engineering, vol. 19, issue 3, 2012, pp. 233–301.
14. Braione P., Denaro G., and Pezz`e M. JBSE: A symbolic executor for java programs with complex heap inputs. In Proc. of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2016, pp. 1018–1022.
15. Reynolds J. C. Separation logic: A logic for shared mutable data structures. In Proc. 17th Annual IEEE Symposium on Logic in Computer Science, 2002, pp. 55–74.
16. Sagiv M., Reps T., and Wilhelm R. Parametric shape analysis via 3-valued logic. ACM Transactions on Programming Languages and Systems, vol. 24, issue 3. 2002, pp. 217–298.
17. Berdine J., Calcagno C., and O’Hearn P.W. Symbolic execution with separation logic. Lecture Notes in Computer Science, vol. 3780, 2005, pp. 52–68.
18. Dudka K., Peringer P., and Vojnar T. Byte-precise verification of lowlevel list manipulation. Lecture Notes in Computer Science, vol. 7935, 2013, pp. 215–237.
19. Barrett C. and Tinelli C. Satisfiability modulo theories. In Handbook of Model Checking, Springer, 2018, pp. 305–343.
20. Kahsai T. et al. Quantified heap invariants for object-oriented programs. In Proc. of the 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 2017, pp. 368– 384.
21. Torlak E. and Bodik R. A lightweight symbolic virtual machine for solver-aided host languages. ACM SIGPLAN Notices, vol. 49, issue 6, 2014, pp. 530–541.
22. Baldoni R. et al. A survey of symbolic execution techniques. ACM Computing Surveys, vol. 51, no. 3, 2018, pp. 50:1-50:39.
23. Unno H., Terauchi T., and Kobayashi N. Automating relatively complete verification of higher-order functional programs. ACM SIGPLAN Notices, vol. 48, issue 1, 2013, pp. 75 86.
24. Zhu H. and Jagannathan S. Compositional and lightweight dependent type inference for ML. Lecture Notes in Computer Science, vol. 7737, 2013, pp. 295–314.
25. Cathcart Burn T., Ong C.-H.L., and Ramsay S. J. Higher-order constrained horn clauses for verification. Proceedings of the ACM on Programming Languages vol. 2, no. POPL, 2017, p. 11:1-11:27.
26. Мандрыкин М.У., Мутилин В.С.. Обзор подходов к моделированию памяти в инструментах статической верификации. Труды ИСПРАН, том 29, вып. 1, 2017 г., стр. 195-230 / Mandrykin M.U., Mutilin V.S. Survey of memory modeling methods in static verification tools. Trudy ISP RAN / Proc. ISP RAS, vol. 29, issue 1, 2017, pp. 195-230 (in Russian). DOI: 10.15514/ISPRAS-2017-29(1)-12.
27. Костюков Ю. О., Батоев К. А., Мордвинов Д. А., Костицын М. П., Мисонижник А. В. Автоматическое доказательство корректности программ с динамической памятью. arXiv:1906.10204, 2019 г. / Kostyukov Yu.O., Batoev K.A., Mordvinov D.A., Kostitsyn M.P., Misonizhnik A.V.. Automatic verification of heap-manipulating programs. arXiv:1906.10204, 2019 (in Russian).
28. Терехов А.Н. Технология программирование встроенных систем. автореферат дис. доктора физико-математических наук. Новосибирск, 1991 г. / Terekhov A.N. Technology for programming of embedded systems. Abstract of Thesis for obtaining the degree of Doctor of physical and mathematical sciences. Novosibirsk, 1991 (in Russian).
29. Новиков Е.М. Развитие ядра операционной системы Linux. Труды ИСП РАН, том 29, вып. 2, 2017 г., стр. 77-96 / Novikov E.M. Evolution of the Linux kernel. Trudy ISP RAN/Proc. ISP RAS, vol. 29, issue 2, 2017, pp. 77-96 (in Russian). DOI: 10.15514/ISPRAS-2017-29(2)-3.
30. Ольхович Л.Б., Кознов Д.В. Метод автоматической валидации UML-спецификаций на языке OCL. Программирование, том 29. № 6, 2003 г., стр. 44-50 / Ol'khovich L., Koznov D.V. OCL-based automated validation method for UML specifications. Programming and Computer Software, vol. 29, № 6, 2003, pp. 323-327.
Review
For citations:
Kostyukov Yu., Batoev K., Mordvinov D., Kostitsyn M., Misonizhnik A. Automatic verification of heap-manipulating programs. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2019;31(5):37-62. (In Russ.) https://doi.org/10.15514/ISPRAS-2019-31(5)-3
Email this article 