Отчёт «Исследование комбинированных методов автоматического анализа программ на наличие ошибок и уязвимостей безопасности» по проекту РФФИ 20-07-00921 (заключительный). Этап 3

Были исследованы существующие подходы по обработке неявных зависимостей в программах при проведении динамического анализа. Большинство современных инструментов (QSYM, SymQEMU, SymCC, Fuzzolic) не учитывают такие зависимости в символьной модели программы, выполняя вместо этого простой перебор значений символьного адреса. Те инструменты, которые поддерживают полноценную интерпретацию неявных зависимостей, либо обладают низкой производительностью из-за особенностей реализации (KLEE, angr), либо являются закрытым коммерческим инструментом (Mayhem). Были разработаны методы для обработки неявных зависимостей по управлению и по данным. Методы были реализованы в инструменте динамического символьного выполнения Sydr, который разрабатывается в ИСП РАН. Среди неявных зависимостей по управлению были выделены табличные условные переходы — косвенная передача управления через табличные преобразования. Табличные условные переходы используются компилятором для компиляции switch выражений в языках Си и Си++. Разработанный метод позволяет инвертировать такие переходы во всех направлениях, его применение на наборе реальных программ позволило обнаружить и инвертировать множество новых символьных переходов. Например, в muraster - разборщике формата pdf, удалось обнаружить 1000 косвенных передач управления через таблицы. Для неявных зависимостей по данным был разработан метод, позволяющий интерпретировать обращения к ячейкам памяти, когда адрес обращения является символьной переменной. Обработка таких зависимостей во время анализа позволяет открывать новые состояния программы, что в свою очередь полезно при фаззинге. Исходя из анализа результатов, предлагаемый подход приводит к небольшому замедлению анализа, но помогает находить много новых символьных ветвей и увеличивает достигнутое покрытие программы. Было проведено исследование существующих подходов к автоматическому обнаружению ошибок с помощью предикатов безопасности (KLEE, Mayhem, SAVIOR, ParmeSan, IntScope) и выявлены их слабые и сильные стороны. Был разработан метод поиска ошибок работы с памятью и неопределенного поведения в программах, использующий гибридный фаззинг и предикаты безопасности. Данный метод был реализован в инструменте Sydr. Метод составляет предикаты безопасности, позволяющие обнаруживать разыменование нулевого указателя, деление на ноль, выход за границы буфера (на стеке и куче) и целочисленное переполнение. Реализованный метод позволил обнаружить 17 неизвестных ранее ошибок в программах с открытым исходным кодом.