Preview

Труды Института системного программирования РАН

Расширенный поиск

Формальная модель обнаружения программных ошибок с помощью символьного исполнения программ

https://doi.org/10.15514/ISPRAS-2019-31(6)-2

Аннотация

Автоматическое обнаружение ошибок в программах является крайне востребованным направлением современных исследований и разработок в области обеспечения безопасности и устойчивости программного обеспечения. В рамках проекта 17-07-00702 Российского фонда фундаментальных исследований исследовались направления применения комбинированных методов анализа программ, совмещающих динамическое символьное исполнение, рандомизированное тестирование и статический анализ программ. Разработаны методы направленного анализа программ, основанные на совмещении статического анализа и динамического символьного исполнения, совмещения рандомизированного тестирования и динамического символьного исполнения программы. В данной статье рассматривается формальная модель обнаружения ошибок в программах методом символьного исполнения программ и её реализация для обнаружения ошибок выхода за границы буфера в памяти. Приводится формальная модель символьного исполнения программ, формулируется и доказывается теорема об обнаружении ошибки в программе, основанная на нарушении области определения операции вычислительной системы. Приводится описание реализации анализатора нарушения границ буфера в памяти в процессе динамического символьного исполнения программы и результаты применения реализованного прототипа анализатора на наборе программ из поставки Debian Linux, подтверждающих применимость предложенного метода обнаружения ошибок.

Об авторах

Александр Юрьевич Герасимов
Институт системного программирования им. В.П. Иванникова РАН
Россия
Какндидат физико-математических наук, старший научный сотрудник


Даниил Олегович Куц
Институт системного программирования им. В.П. Иванникова РАН
Россия
Aспирант ИСП РАН


Александр Андреевич Новиков
Институт системного программирования им. В.П. Иванникова РАН
Россия
Aспирант ИСП РАН


Список литературы

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.


Рецензия

Для цитирования:


Герасимов А.Ю., Куц Д.О., Новиков А.А. Формальная модель обнаружения программных ошибок с помощью символьного исполнения программ. Труды Института системного программирования РАН. 2019;31(6):21-32. https://doi.org/10.15514/ISPRAS-2019-31(6)-2

For citation:


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



Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 2079-8156 (Print)
ISSN 2220-6426 (Online)