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


Обнаружение ошибок доступа к буферу в программах на языке C/C++ с помощью статического анализа

И.А. Дудина (ИСП РАН, Москва, Россия, МГУ, Москва, Россия)

Аннотация

В данной работе рассматривается метод поиска межпроцедурных ошибок доступа к буферу с помощью статического анализа. В основе рассматриваемого подхода лежит разработанный ранее алгоритм внутрипроцедурного анализа на базе символьного исполнения с объединением состояний, который является чувствительным к путям и учитывает взаимосвязи между переменными, такие как сравнения, арифметические операции и инструкции приведения типа. В работе предложено формальное определение межпроцедурного дефекта и рассмотрены некоторые типы межпроцедурных ошибок доступа к буферу. Межпроцедурный анализ реализован с помощью метода резюме, что позволяет в некоторой степени добиться контекстной чувствительности. Показано, как можно расширить внутрипроцедурный алгоритм для отслеживания межпроцедурных связей между переменными. Кроме этого, приведен алгоритм построения двух типов достаточных условий наличия ошибки доступа к буферу в функции, которые сохраняются в резюме и проверяются при вызове этой функции. Описанный подход был реализован в инструменте статического анализа Svace. На проекте Android 5.0.2 было получено 351 предупреждение об ошибке доступа к буферу, среди которых 64% оказались истинными, при этом существенного замедления анализа не произошло.

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

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

Издание

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

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

DOI: 10.15514/ISPRAS-2016-28(5)-7

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