DOI: 10.17586/2226-1494-2020-20-1-101-109


УДК004.052.42

ПОДХОД К ВЕРИФИКАЦИИ АЛЛОКАТОРОВ ДИНАМИЧЕСКОЙ ПАМЯТИ, ОСНОВАННЫЙ НА СИМВОЛЬНОМ ВЫПОЛНЕНИИ ПРОГРАММ

Дергачев А.М., Садырин Д.С., Ильина А.Г., Логинов И.П., Кореньков Ю.Д.


Читать статью полностью 
Язык статьи - русский

Ссылка для цитирования:
Дергачев А.М., Садырин Д.С., Ильина А.Г., Логинов И.П., Кореньков Ю.Д. Подход к верифика- ции аллокаторов динамической памяти, основанный на символьном выполнении программ // Научно-технический вестник информационных технологий, механики и оптики. 2020. Т. 1. № 1. С. 101–109. doi: 10.17586/2226-1494-2020-20-1-101-109


Аннотация
Предмет исследования. Исследованы техники эксплуатации уязвимостей в реализации алгоритмов распределения динамической памяти – аллокаторе библиотеки glibc (Poisoned Null-byte, Overlapped Chunks, Fastbin Attack, Unsafe Unlink, House of Einherjar, House of Force, House of Spirit, House of Lore, Unsorted Bin Attack). Приведены примеры кода эксплуатации уязвимостей и классификация представленных техник в соответствии с общим перечнем Common Weakness Enumeration. Исследованы современные методы и средства обнаружения уязвимостей, показаны их достоинства и недостатки на примере работы фреймворка Heap Hopper. Рассмотрены современные подходы к верификации программного обеспечения. Метод. Предложенный метод верификации программного обеспечения совмещает подходы статического анализа и символьного выполнения при использовании точной модели алгоритмов выделения динамической памяти. В процессе компиляции проверяемой программы создается структура Крипке. Уязвимости динамической памяти описываются формулами темпоральной логики. Полученная структура и формулы передаются на вход алгоритма проверки моделей. Осуществляется конкретно-символьное выполнение собранного бинарного файла. Для символьных путей выполнения проверяются условия уязвимостей, выраженные в виде формул пропозициональной логики. Основные результаты. Показана возможность практического применения предложенного подхода к обнаружению уязвимостей, возникающих при распределении динамической памяти в программных приложениях. Символьное выполнение реализовано в виде низкоуровневого отладчика, что позволяет снизить время работы алгоритмов за счет выполнения проверяемого приложения на реальном процессоре. Практическая значимость. Представлен комплексный подход для решения проблемы автоматического выявления уязвимостей на разных стадиях жизненного цикла разработки программного обеспечения. Предложенный подход применим для верификации аналогичных реализаций аллокаторов динамической памяти, таких как ptmalloc, dlmalloc, tcmalloc, jemalloc, musl.

Ключевые слова: верификация, уязвимость, символьное выполнение, динамическая память, язык С

Список литературы
1. Андреев Ю.С., Дергачев А.М., Жаров Ф.А., Садырин Д.С. Информационная безопасность автоматизированных систем управления технологическими процессами // Известия высших учебных заведений. Приборостроение. 2019. Т. 62. № 4. С. 331–
339. doi: 10.17586/0021-3454-2019-62-4-331-339
2. Щеглов К.А., Щеглов А.Ю. Эксплуатационные характеристики риска нарушений безопасности информационной системы // Научно-технический вестник информационных технологий, механики и оптики. 2014. № 1(89). С. 129–139.
3. Repel D., Kinder J., Cavallaro L. Modular synthesis of heap exploits // Proc. of the 2017 Workshop on Programming Languages and Analysis for Security, PLAS’17. 2017. P. 25–35. doi: 10.1145/3139337.3139346
4. Heelan S., Melham T., Kroening D. Automatic heap layout manipulation for exploitation // Proc. 27th USENIX Security Symposium. 2018. P. 763–779.
5. Liu D., Zhang M., Wang H. A robust and efficient defense against use-after-free exploits via concurrent pointer sweeping // Proc. 25th ACM Conference on Computer and Communications Security (CCS 2018). 2018. P. 1635-1648. doi: 10.1145/3243734.3243826
6. Nikiforakis N., Piessens F., Joosen W. HeapSentry: Kernel-assisted protection against heap overflows // Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2013. V. 7967. P. 177–196. doi: 10.1007/978-3-642-39235-1_11
7. Lee B., Song C., Jang Y., Wang T., Kim T., Lu L., Lee W. Preventing use-after-free with dangling pointers nullification [Электронный ресурс]. URL: https://wenke.gtisc.gatech.edu/papers/dangnull.pdf, свободный. Яз. англ. (дата обращения: 15.01.2020). doi: 10.14722/ndss.2015.23238
8. Novark G., Berger E.D. DieHarder: Securing the heap // Proc. 17th ACM Conference on Computer and Communications Security, CCS’10. 2010. P. 573–584. doi: 10.1145/1866307.1866371
9. Caballero J., Grieco G., Marron M., Nappa A. Undangle: Early detection of dangling pointers in use-after-free and double-free vulnerabilities // Proc. 21st International Symposium on Software Testing and Analysis (ISSTA 2012). 2012. P. 133–143. doi: 10.1145/04000800.2336769
10. Atzeni A., Marcelli A., Muroni F., Squillero G. HAIT: Heap analyzer with input tracing // ICETE 2017 – Proc. 14th International Joint Conference on e-Business and Telecommunications. 2017. V. 4. P. 327–334. doi: 10.5220/0006420803270334
11. Yun I., Karil D., Kim T. Automatic techniques to systematically discover new heap exploitation primitives [Электронный ресурс]. URL: https://arxiv.org/pdf/1903.00503.pdf, свободный. Яз. англ. (дата обращения: 15.01.2020).
12. Chen H., Wagner D. MOPS: An infrastructure for examining security properties of software // Proc. 9th ACM Conference on Computer and Communications Security. 2002. P. 235–244. doi: 10.1145/586110.586142
13. Clarke E., Kroening D., Lerda F. A tool for checking ANSI-C programs
// Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 2004. V. 2988. P. 168–176. doi: 10.1007/978-3-540-24730-2_15
14. Eckert M, Bianchi A, Wang R, Shoshitaishvili Y, Kruegel C, Vigna G. HeapHopper: Bringing bounded model checking to heap implementation security // Proc. 27th USENIX Security Symposium. 2018. P. 99–116.
15. Xu W., DuVarney D.C., Sekar R. An efficient and backwards- compatible transformation to ensure memory safety of C programs // Proc. Twelfth ACM SIGSOFT International Symposium on the Foundations of Software Engineering, SIGSOFT 2004/FSE-12. 2004. P. 117–126. doi: 10.1145/1029894.1029913
16. Yet another free() exploitation technique [Электронный ресурс]. URL: http://phrack.org/issues/66/6.html, свободный. Яз. англ. (дата обращения: 15.01.2020).
17. Malloc Des-Maleficarum [Электронный ресурс]. URL: http://www. phrack.org/issues/66/10.html, свободный. Яз. англ. (дата обращения: 15.01.2020).
18. A repository for learning various heap exploitation techniques [Электронный ресурс]. URL: https://github.com/shellphish/ how2heap, Яз. англ. (дата обращения: 15.01.2020).
19. Dudina I.A., Belevantsev A.A. Using static symbolic execution to detect buffer overflows // Programming and Computer Software. 2017. V. 43. N 5. P. 277–288. doi: 10.1134/S0361768817050024
20. Ермаков М.К. Методы повышения эффективности итеративного динамического анализа программ: диссертация на соискание ученой степени кандидата математических наук. М.: Московский государственный университет им. М.В. Ломоносова, 2016.
21. Wang F., Yan S. Angr - the next generation of binary analysis // Proc. IEEE Cybersecurity Development Conference (SecDev 2017). 2017. P. 8–9. doi: 10.1109/SecDev.2017.14
22. Kripke structure (model checking) [Электронный ресурс]. URL: https://en.wikipedia.org/wiki/Kripke_structure_(model_checking) свободный. Яз. англ. (дата обращения: 15.01.2020).
23. Bhat G., Cleaveland R., Grumberg O. Efficient on-the-fly model checking for CTL // Proc. 10th Annual IEEE Symposium on Logic in Computer Science. 1995. P. 388–397. doi: 10.1109/LICS.1995.523273
24. Saudel F., Salwan J. Triton: A dynamic symbolic execution framework // Symposium sur la sécurité des technologies de l’information et des communications, SSTIC, France, Rennes. 2015. P. 31–54.
 


Creative Commons License

This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License
Информация 2001-2020 ©
Научно-технический вестник информационных технологий, механики и оптики.
Все права защищены.

Яндекс.Метрика