A formal model for program defect detection using symbolic program execution
https://doi.org/10.15514/ISPRAS-2019-31(6)-2
Abstract
An automatic program defect detection is extremely important direction of current research and development in the field of program reliability and security assurance. There were performed research of different ways of application for combined analysis methods which mix static source code analysis and dynamic symbolic execution, fuzz testing and dynamic symbolic execution as part of previous period of two years for project 17-07-00702 of the Russian Foundation for Basic Research. This paper presents elaboration of previously presented methods in form of formal model of program symbolic execution applied for program defect detection and implementation of analyzer of memory buffer bounds violation based on this model. The common theorem for program defect detection based on model of symbolic program execution and violation of definitional domain for computation system operation is formulated and proved. A special case theorem for buffer bounds violation detection is formulated and proved basing on common theorem and shadow memory model. As a practical application for theoretical basis an implementation of the analysis tool prototype description provided. Experimental results are received on the set of command line utilities of Debian Linux distribution, which shows applicability of proposed theoretical basis for solving practical tasks in the field of program reliability and security assurance.
Supporting agencies: The research was supported by RFBR. Grant No. 17-07-00702.
About the Authors
Alexander Yurievich Gerasimov
Ivannikov Institute for System Programming of the Russian Academy of Sciences
Russian Federation
PhD in Computer Sciences, senior researcher
Russian Federation
PhD in Computer Sciences, senior researcher
Daniil Olegovich Kuts
Ivannikov Institute for System Programming of the Russian Academy of Sciences
Russian Federation
PhD Student at ISP RAS
Russian Federation
PhD Student at ISP RAS
Alexander Andreevich Novikov
Ivannikov Institute for System Programming of the Russian Academy of Sciences
Russian Federation
PhD Student at ISP RAS
Russian Federation
PhD Student at ISP RAS
References
1. B. P. Miller, L. Fredriksen, B. So. An empirical study of the reliability of UNIX utilities. Communications of the ACM, vol. 33, issue 12, 1990, pp. 32- 44.
2. M. Zalewski. Symbolic execution in vuln research. Available at: https://lcamtuf.blogspot.com/2015/02/symbolic-execution-in-vuln-research.html, 23.12.2019.
3. R.S. Boyer, B. Elspas, K.N. Levitt. SELECT – F Formal System for Testing and Debugging Programs by Symbolic Execution. In Proc. of the International Conference on Reliable software, 1975, pp. 234-245.
4. А.Ю. Герасимов, Л.В. Круглов. Вычисление входных данных для достижения определенной функции в программе методом итеративного динамического анализа. Труды ИСП РАН, том 28, вып. 5, 2016, стр. 159-174 / A.Y. Gerasimov, L.V. Kruglov. Input data generation for reaching specific function in program by iterative dynamic analysis method. Trudy ISP RAN/Proc. ISP RAS, vol. 28, issue 5, 2016, pp. 159-174 (in Russian). DOI: 10.15514/ISPRAS-2016-28(5)-10.
5. Герасимов А.Ю., Круглов Л.В., Ермаков М.К., Вартанов С.П. Подход определения достижимости программных дефектов, обнаруженных методом статического анализа программ, при помощи динамического анализа. Труды ИСПРАН, том 29, вып. 5, 2017 г., стр. 111-134 / Gerasimov A.Y., Kruglov L.V., Ermakov M.K., Vartanov S.P. An approach of reachability confirmation for static analysis defects with help of dynamic symbolic execution. Trudy ISP RAN/Proc. ISP RAS, vol. 29, issue 5, 2017. pp. 111-134 (in Russian). DOI: 10.15514/ISPRAS-2017-29(5)-7.
6. Godefroid P., Levin M. Y., Molnar D. SAGE: whitebox fuzzing for security testing. Communications of the ACM. vol. 55, issue 3, 2012, pp. 40-44.
7. CWE-476: NULL Pointer Dereference. Available at: https://cwe.mitre.org/data/definitions/476.html, accessed: 23.12.2019.
8. CWE-121: Stack-based Buffer Overflow. Available at: https://cwe.mitre.org/data/definitions/121.html, accessed: 23.12.2019.
9. CWE-122: Heap-based Buffer Overflow. Available at: https://cwe.mitre.org/data/definitions/122.html, accessed: 23.12.2019.
10. CWE-123: Write-what-where Condition. Available at: https://cwe.mitre.org/data/definitions/123.html, accessed: 23.12.2019.
11. CWE-125: Out-of-bounds Read. Available at: https://cwe.mitre.org/data/definitions/125.html, accessed: 23.12.2019.
12. CWE-787: Out-of-bounds Write. Available at: https://cwe.mitre.org/data/definitions/787.html, accessed: 23.12.2019.
13. A. Gerasimov, S.Vartanov, M. Ermakov, L. Kruglov, D. Kutz, A. Novikov, S. Asryan. Anxiety: a dynamic symbolic execution framework. In Proc. of the 2017 Ivannikov ISPRAS Open Conference, 2017, pp. 16-21. DOI: 10.1109/ISPRAS.2017.00010
14. Федотов А.Н., Каушан В.В., Гайсарян С.С., Курмангалеев Ш.Ф. Построение предикатов безопасности для некоторых типов программных дефектов. Труды ИСП РАН, том 29, вып. 6, 2017 г., стр. 151-162 / Fedotov A.N., Kaushan V.V., Gaissaryan S.S., Kurmangaleev Sh.F. Building security predicates for some types of vulnerabilities. Trudy ISP RAN/Proc. ISP RAS, vol. 29, issue 6, 2017. pp. 151-162 (in Russian). DOI: 10.15514/ISPRAS-2017-29(6)-8.
15. D. Bruening, T. Garnett, S. Amarasinghe. An infrastructure for adaptive dynamic optimization. In Proc. of the International Symposium on Code Generation and Optimization, 2003, pp. 265-275.
Review
For citations:
Gerasimov A.Yu., Kuts D.O., Novikov A.A. A formal model for program defect detection using symbolic program execution. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2019;31(6):21-32. (In Russ.) https://doi.org/10.15514/ISPRAS-2019-31(6)-2
Email this article 