Up

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

[Svace] Поиск ошибок доступа к буферу в программах на языке C/C++
1 · 2 · 3 · 4 · 5 · 6 · 7 · 8 — 14

2016+. И. А. Дудина, В. К. Кошелев, А. Е. Бородин. Ещё не опубликована. См. Svace.

1 Здесь определяются достаточные условия выхода за границы массива. Но нам нужны необходимые? 2 Задача в общем случае алгоритмически неразрешима. 3 Рассматриваются только константные буферы (размер известен на момент компиляции). 4 Каждая функция считается точкой входа в программу, для поиска дефектов во всех потенциальных контекстах вызова (а не только на уже существующих). (Это актуально в основном для библиотечных функций.) Неизвестные переменные функции: входные параметры, начальное состояние памяти, результаты вызываемых функций. Ограничения на множество НПконтракт.

5 По условию, контракты не известны. Но для каждой ошибки можно подобрать такой к функции контракт, что ошибка исчезнет. Поэтому они будут пытаться искать такие ошибки, которые зависят от свойств ГПУ (есть путь, на котором ошибка гарантировано будет), но не зависят от множества НП. 6 Контракты не должны сужать множество выполнимых путей.

7 Ядро Svace проводит символьное исполнение программы с объединением состояний. 8 Решение: в ходе символьного исполнения проводить VSA, проверять выполнимость формулы потенциального дефекта (т. е. они делают то же самое, что и мы, только в статике):

ReachCond(instr) and (NotLess(instr, index, size) or NotGreater(instr, index, -1))

14 При реализации в качестве инструкций доступа к буферу рассматривались обычные инструкции индексации и вызовы библиотечных функций (например, memcpy).

[Выше уже было отмечено, что] [т.е., т.о.] [путь на ГПУ ? в ГПУ]

18 pages

Sergey Vartanov, 2007–2020