Сборники трудов ИСП РАН


Поиск ошибок доступа к буферу в программах на языке C/C++

И.А. Дудина (ИСП РАН, Москва, Россия; МГУ, Москва, Россия)
В.К. Кошелев (ИСП РАН, Москва, Россия)
А.Е. Бородин (ИСП РАН, Москва, Россия)

Аннотация

В статье рассматривается алгоритм статического анализа для поиска в исходном коде программы ошибок доступа к буферу. Алгоритм использует символьное исполнение с объединением состояний и является чувствительным к путям. Рассматриваются только обращения к буферам, имеющим известный в момент компиляции размер и размещённым в статической памяти либо на стеке. В работе приведено формальное определение ошибки доступа к буферу, возникающей при прохождении некоторой последовательности рёбер графа потока управления программы. Приведён алгоритм, позволяющий для переменных программы суммировать информацию о возможных значениях по всем путям с учётом совместности условий переходов, взаимосвязи переменных через арифметические операции, инструкции преобразования типов, бинарные отношения в условиях переходов. Для инструкций доступа к буферу с помощью вычисленной для переменной индекса информации о возможных значениях вычисляются достаточные условия выхода за границы. Выполнимость достаточных условий проверяется SMT-решателем и, в случае нахождения модели, с её помощью обнаруживается ошибочный путь и выдаётся предупреждение. На основе данного подхода в инструменте статического анализа Svace был реализован межпроцедурный чувствительный к путям детектор ошибок доступа к буферу, способный обнаруживать новые, не покрытые предыдущими реализациями детекторов типы ошибок.

Ключевые слова

статический анализ; поиск дефектов; переполнение буфера; чувствительность к путям; символьное исполнение

Издание

Труды Института системного программирования РАН, том 28, вып. 4, 2016, стр. 149-168.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2016-28(4)-9

Полный текст статьи в формате pdf Вернуться к содержанию тома