Отчёт "Исследование и разработка программной инфраструктуры для анализа бинарного кода, настраиваемой по целевой процессорной архитектуре" по проекту РФФИ 18-07-01256 (итоговый).

Целью проекта является создание универсальной инфраструктуры анализа бинарного кода, которая может применяться в качестве базового компонента в широком спектре инструментов анализа и при этом обеспечивать независимость таких инструментов от целевой процессорной архитектуры анализируемого бинарного кода за счет декодирования машинных команд и их трансляции в машинно-независимое промежуточное представление. В рамках проекта выполнено исследование особенностей современных процессорных архитектур и проведен обзор существующих подходов к моделированию операционной семантики процессорных команд. Разработано и реализовано в виде программного компонента промежуточное представление, позволяющее более точно описывать такого рода модели, в особенности в части выборки команд (слоты задержки, аппаратная поддержка циклов и т.п.), доступа к памяти и системных команд. Трансляция машинных команд в данное промежуточное представление управляется внешними спецификациями на разработанном в ходе проекта предметно-ориентированном языке и включает в себя компонент для декодирования машинных команд, основанный на автомате с магазинной памятью. Реализованы и отлажены частичные спецификации для процессорных архитектур x86, RISC-V, MIPS, PowerPC и др. Инфраструктура позволяет строить промежуточное представление как по бинарному образу исследуемых программ, так и по заранее записанным трассам выполнения. Дальнейший анализ проводится в терминах математического аппарата абстрактной интерпретации: инфраструктура содержит компоненты как для интерпретации отдельных путей в программе, так и для поиска неподвижной точки в задаче статического анализа. Для проведения анализа пользователю инфраструктуры достаточно задать абстрактный домен, передаточные функции и начальное состояние; определение порядка применения передаточных функций и построение вспомогательных структур данных (например, графа потока управления) инфраструктура выполнит автоматически. В состав инфраструктуры включены наиболее универсальные виды интерпретации: конкретная, символьная и смешанная (concolic). Работоспособность системы проверена в ряде экспериментов, где применялось смешанное выполнение для автоматического определения входных данных программ, приводящих их в заданные состояния. Были получены корректные решения, а производительность разработанной в рамках проекта инфраструктуры оказалась сравнима со специализированными системами символьного выполнения, не основанными на внешних спецификациях.