Институт системного программирования им. В.П. Иванникова РАН

BINSIDE. Инструмент обнаружения дефектов в программе методами статического анализа исполняемого кода

Бинарный статический анализ

Бинарный статический анализ необходим в тех случаях, когда нет доступа к исходному коду, например, при анализе библиотек. Статический анализатор бинарного кода разрабатывается на основе фреймворка BinNavi. Для удобства пользователя анализатор интегрирован в IDA PRO. Поддерживается анализ бинарных файлов и библиотек архитектур x86, x64, ARM, PowerPC и MIPS. Бинарный файл дизассемблируется и передается BinNavi. BinNavi, переводит ассемблерный код в собственное представление, называемое REIL. Представление REIL содержит семнадцать инструкций без побочных эффектов. Каждая ассемблерная инструкция транслируется в набор из REIL инструкций. Язык промежуточного представления REIL позволяет анализировать код независимо от процессорной архитектуры и операционной системы, для которых была написана программа. Кроме того, BinNavi обеспечивает навигацию по графам потока управления, графам потока данных и графу вызовов программы. В рамках анализатора бинарного кода реализован плагин для статического анализа патчей программ.

Работа плагинов поиска уязвимостей основана на интервальном анализе, отслеживании помеченных данных, моделях статической и динамической памяти, анализе графов потока данных и управления.

На основе среды BinNavi был реализован поиск двух типов переполнения буфера на стеке в виде плагинов. Первый тип переполнения возникает при копировании информации из большего буфера в меньший. Такой тип переполнения возникает при использовании таких небезопасных функций, как strcpy, memcpy и т. д. Второй тип переполнения возникает при копировании одного буфера в другой без проверки границ первого буфера, например, пока не встретится символ конца строки. В обоих случаях основным критерием наличия уязвимости является возможность получения контроля над входным буфером. Кроме того реализован поиск уязвимостей форматной строки и ошибок работы с указателями. Инструмент демонстрирует неплохие показатели по скорости работы. На бинарном файле из более 3000 функций анализ длится около 2000 сек.

Статический анализ исходного кода

Инструмент Svace осуществляет статический поиск дефектов, используя несколько видов анализаторов. Текущая версия Svace для анализа С и С++ программ содержит статические анализаторы двух уровней: легковесный анализатор и основной анализатор. Легковесный анализатор, интегрированный в компилятор Clang, осуществляет поиск дефектов, в процессе обхода абстрактного синтаксического дерева. Более сложный анализатор осуществляет межпроцедурный потоково- и контекстно-чувствительный анализ. Основной анализатор осуществляет межпроцедурный анализ путём обхода графа вызовов «снизу-вверх», начиная с листьев графа таким образом, чтобы вызываемые функции анализировались до вызывающих. Каждая функция обходится только один раз, вся необходимая в дальнейшем информация помещается в специальную структуру данных, называемую аннотацией. Такой подход позволяет анализировать каждую функцию только один раз, что существенно улучшает скорость анализа и масштабируемость.

При анализе каждой функции создаётся граф потока управления и производится его топологическая сортировка. Затем осуществляется анализ 2-х видов: консервативный анализ потока данных и неконсервативный анализ, использующий сложную модель памяти. В процессе анализа осуществляется как прямой, так и обратный топологический обход графа потока управления. Задача каждого из проходов собрать факты о том, что произойдёт или может произойти с переменной. Классическим примером обратного прохода является анализ живых определений переменных, целью которого является разграничение областей программы, в рамках которых значение переменной не изменяется. Неконсервативный анализ имеет поддержку чувствительности к путям, контексту и поддерживает межпроцедурный анализ. Ядро анализатора поддерживает возможность проводить анализ разной степени сложности, а использование этих возможностей зависит от конкретного детектора. Благодаря этому для каждого детектора можно выбрать необходимую степень учитываемых свойств.

Инструмент Svace имеет приемлемые характеристики времени анализа проектов и соотношения истинных и ложно-истинных предупреждений. Детекторы Svace имеют долю истинных предупреждений от 69 до 95%. Детекторы из легковесного анализатора имеют больший процет истинных предупреждений. Общее время для сборки и анализа должно позволять проводить анализ во время ночной сборки. Время анализа для небольших проектов (busybox, cairo, dnprogs) составляет около 5 минут на рабочей станции разработчика, что сопоставимо со временем сборки. Анализ операционной системы Android 5.0.2 на сервере с 256 ГБ оперативной памяти занимает около 5 часов. Сборка андроида занимает 2,5 часа. Таким образом общее время, необходимое на сборку и анализ андроида составляет 7,5 часов, что является приемлемым для ежедневного анализа во время ночной сборки проекта.

Разработчик/участник

Компиляторные технологии