Preview

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

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

Практическая абстрактная интерпретация бинарного кода

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



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


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