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 ©
Научно-технический вестник информационных технологий, механики и оптики.
Все права защищены.

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