Практическая абстрактная интерпретация бинарного кода
https://doi.org/10.15514/ISPRAS-2020-32(6)-8
Аннотация
Математический аппарат абстрактной интерпретации предоставляет универсальный способ формализации и изучения алгоритмов анализа программ для самого широкого спектра прикладных задач. Однако его применение для практически значимых задач анализа бинарного кода связано с большим числом вызовов, как научных, так и инженерных. В настоящей работе предложены подходы к преодолению части этих трудностей. Описано промежуточное представление, учитывающее особенности бинарного кода. Предложена инфраструктура абстрактной интерпретации с возможностью выполнения интерпретации как вдоль отдельного пути в программе, так и статически до достижения неподвижной точки. В совокупности промежуточное представление и инфраструктура абстрактной интерпретации позволяют задать модель конвейера процессора, что позволяет проводить анализ бинарного кода для различных архитектур. В работе также представлены предварительные эксперименты и указаны дальнейшие направления развития проекта.
Ключевые слова
Об авторах
Михаил Александрович СОЛОВЬЕВРоссия
Кандидат физико-математических наук, старший научный сотрудник отдела компиляторных технологий ИСП РАН; старший преподаватель кафедры системного программирования факультета ВМК МГУ
Максим Геннадьевич БАКУЛИН
Россия
Младший научный сотрудник отдела компиляторных технологий
Сергей Сергеевич МАКАРОВ
Россия
Студент кафедры системного программирования
Дмитрий Валерьевич МАНУШИН
Россия
Аспирант кафедры системного программирования
Вартан Андроникович ПАДАРЯН
Россия
Кандидат физико-математических наук, ведущий научный сотрудник отдела компиляторных технологий ИСП РАН; доцент кафедры системного программирования факультета ВМК МГУ
Список литературы
1. Cousot P, 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.
2. Kildall G. A unified approach to global program optimization. In Proc. of the 1st ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, 1973, pp. 194-206.
3. Mauborgne L. ASTRÉE: Verification of Absence of Run-Time Error. In Building the information society, IFIP International Federation for Information Processing, vol. 156, 2004, pp. 384-392.
4. Соловьев М.А., Бакулин М.Г., Горбачев М.С., Манушин Д.В., Падарян В.А., Панасенко С.С. О новом поколении промежуточных представлений, применяемом для анализа бинарного кода. Труды ИСП РАН, том 30, вып. 6, 2018, стр. 39-68 / Solovev M.A., Bakulin M.G., Gorbachev M.S., Manushin D.V., Padaryan V.A., Panasenko S.S. Next generation intermediate representations for binary code analysis. Trudy ISP RAN/Proc. ISP RAS, vol. 30, issue 6, 2018, pp. 39-68 (in Russian). DOI: 10.15514/ISPRAS-2018-30(6)-3.
5. Dullien T., Porst S. REIL: A platform-independent intermediate representation of disassembled code for static code analysis. In Proc. of the CanSecWest Conference, 2009, 7 p.
6. Jung M., Kim S., Han H., Choi J., Cha S.K. B2R2: building an efficient front-end for binary analysis. In Proc. of the NDSS workshop on Binary analysis research, 2019, 10 p.
7. Cruehead. URL: https://ansmirnov.ru/crackme-cruehead/ (in Russian), accessed: 23.10.2020.
8. The Z3 Theorem Prover. URL: https://github.com/Z3Prover/z3, accessed: 23.10.2020.
9. Boolector. URL: https://boolector.github.io/, accessed: 23.10.2020.
Рецензия
Для цитирования:
СОЛОВЬЕВ М.А., БАКУЛИН М.Г., МАКАРОВ С.С., МАНУШИН Д.В., ПАДАРЯН В.А. Практическая абстрактная интерпретация бинарного кода. Труды Института системного программирования РАН. 2020;32(6):101-110. https://doi.org/10.15514/ISPRAS-2020-32(6)-8
For citation:
SOLOVEV M.A., BAKULIN M.G., MAKAROV S.S., MANUSHIN D.V., PADARYAN V.A. Practical Abstract Interpretation of Binary Code. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2020;32(6):101-110. (In Russ.) https://doi.org/10.15514/ISPRAS-2020-32(6)-8