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