[Svace] Поиск ошибок доступа к буферу в программах на языке C/C++
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