RUS  ENG
Полная версия
ЖУРНАЛЫ // Труды института системного программирования РАН // Архив

Труды ИСП РАН, 2021, том 33, выпуск 1, страницы 7–32 (Mi tisp569)

Эта публикация цитируется в 3 статьях

Поиск уязвимостей небезопасного использования помеченных данных в статическом анализаторе Svace

А. Е. Бородинa, А. В. Горемыкинba, С. П. Вартановa, А. А. Белеванцевba

a Институт системного программирования им. В.П. Иванникова РАН
b Московский государственный университет имени М.В. Ломоносова

Аннотация: В статье рассматривается поиск ошибок помеченных данных в исходном коде программ, т.е. ошибок, вызванных небезопасным использованием данных, полученных из внешних источников, которые потенциально могут быть изменены злоумышленником. В качестве основы использовался межпроцедурный статический анализатор Svace. Анализатор осуществляет как поиск дефектов в программе, так и поиск подозрительных мест, в которых логика программы может быть нарушена. Целью является найти как можно больше ошибок при приемлемой скорости и низком уровне ложных срабатываний (< 20–35%). Для поиска ошибок Svace с помощью компилятора строит низкоуровневое типизированное промежуточное представление, которое подаётся на вход основному анализатору SvEng. Анализатор строит граф вызовов, после чего выполняет анализ на основе резюме. При таком анализе функции обходятся в соответствии с графом вызовов, начиная с листьев. После анализа функции создаётся её резюме, которое затем будет использовано для анализа инструкций вызова. Анализ имеет как высокую скорость, так и хорошую масштабируемость. Внутрипроцедурный анализ основан на символьном выполнении с объединением состояний в точках слияния путей. Для отсеивания несуществующих путей для некоторых детекторов может использоваться SMT-решатель. При этом SMT-решатель вызывается, только если есть подозрение на ошибку. Анализатор был расширен возможностью поиска дефектов, связанных с помеченными данными. Детекторы реализованы в виде плагинов по схеме источник-приёмник. В качестве источников используются вызовы библиотечных функций, получающих данные извне программы, а также аргументы функции main. Приёмниками являются обращение к массивам, использование переменных как шага или границы цикла, вызов функций, требующих проверенных аргументов. Реализованы детекторы, покрывающие большинство возможных типов уязвимостей, для непроверенных целых чисел и строк. Для оценки покрытия использовался проект Juliet. Уровень пропусков составил от 46.31% до 81.17% при незначительном количестве ложных срабатываний.

Ключевые слова: статический анализ, символьное выполнение, анализ помеченных данных, Svace, поиск ошибок, уязвимости.

DOI: 10.15514/ISPRAS-2021-33(1)-1



© МИАН, 2024