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

Математический аппарат абстрактной интерпретации предоставляет универсальный способ формализации и изучения алгоритмов анализа программ для самого широкого спектра прикладных задач. Однако его применение для практически значимых задач анализа бинарного кода связано с большим числом вызовов, как научных, так и инженерных. В настоящей работе предложены подходы к преодолению части этих трудностей. Описано промежуточное представление, учитывающее особенности бинарного кода. Предложена инфраструктура абстрактной интерпретации с возможностью выполнения интерпретации как вдоль отдельного пути в программе, так и статически до достижения неподвижной точки. В совокупности промежуточное представление и инфраструктура абстрактной интерпретации позволяют задать модель конвейера процессора, что позволяет проводить анализ бинарного кода для различных архитектур. В работе также представлены предварительные эксперименты и указаны дальнейшие направления развития проекта.

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.