МГУ имени Ломоносова, механико-математический факультет, кафедра вычислительной математики Исследование проблемы переполнения буферов в программах Пучков Ф.М. Шапченко К.А. Москва, 2004 г.

Влияние переполнения буферов на стек Arg2 IP B[ ] A.. Arg1 SP (Stack Pointer) Адрес возврата в вызвавшую функцию(адрес следующей инструкции, Instruction Pointer) При переполнении может произойти изменение адреса возврата Стек растет вниз Направление увеличения адресов стека Аргументы функции. Заносятся в стек в обратном порядке..... Начало стека

Принцип работы алгоритма Си-программа Блок-схемы + достаточные условия корректности Информационная база Выявление подозрительных мест Алгоритм преобразования в блок-схему Анализ блок- схемы Вывод Реальные переполнения Ложные тревоги Основные направления модификации алгоритмов работы В глубину (то есть расширение класса СИ-программ, корректность работы которых сводится к исследованию конечного числа блок-схем, а также совершенствование алгоритмов вывода) В ширину (то есть реализация дополнительных алгоритмов, генерирующих условия информационной базы)

Демонстрация работы алгоритма int main() { int i; int a[10]; i=0; while ( a[i] >= 0 ) i=i+1; return 0; } int main() { int i,k; int a[10]; for ( i=0; i

START P(i) : 0 i

int main() { int i,k; int a[10]; for ( i=0; i

Преобразование СИ-программы в блок-схему Ассоциированные переменные – Границы памяти для указателей – Области перекрытия указателей Язык представления блок-схемы Построение блок-схемы по исходному тексту программы Генерация условий для проверки – Обращения к элементам массива по индексу – Обращения к памяти по указателю

Язык представления блок-схемы Нумерованный список инструкций 4 типов Присваивание A = Условный переход C # : Безусловный переход G Инструкция конца программы S

Построение блок-схемы по исходному тексту Предварительная обработка исходного текста – Упрощение некоторых языковых конструкций – Операции с ассоциированными переменными Обработка вызовов функций – Встраивание функций – Аннотирование аргументов и возвращаемых значений – Рекурсивные функции Преобразование в язык представления блок-схемы

Пример преобразования int f(int * array, int index) { return array[index]; } int main(void) { int i, n, b; int * a; n = 10; a = (int*) malloc (n * sizeof(int)); for (i=0; i

Принцип работы алгоритма Си-программа Блок-схемы + достаточные условия корректности Информационная база Выявление подозрительных мест Алгоритм преобразования в блок-схему Анализ блок- схемы Вывод Реальные переполнения Ложные тревоги

Структура информационной базы Система 1 : Система 2 : Система s : Условие коррекности должно выполняться в каждой из s систем.

Алгоритмы создания информационной базы Предобработка блок-схемы (приоритет 3) - возможность выборочной предобработки Алгоритм «минимальных наборов» (приоритет 4) Использование системных переменных (приоритет 2) - системные переменные первого типа - системные переменные второго типа Доказательство обратных оценок (приоритет 4) Эвристические алгоритмы генерации условий (приоритет 1) - геометрическая классификация блок-схем - разбиение блок-схемы на части

Алгоритмы создания информационной базы Условия, сгенерированные алгоритмом (в точке X) : i < 10 k < i i 0 k 0 Условия (1) и (2) получены методом мнимальных наборов, а условия (3) и (4) доказаны как обратные оценки. (1) (2) (3) (4) X START i < 10 k < i STOP i = 0 P(i) : 0 i

Математическая модель Блок-схема - – множество переменных; - – множество параметров; - G=(V, E) – конечный ориентированный граф, F={START, STOP, FAULT}; - – набор предикатов - – набор подстановок

Математическая модель - автономный недетерминированный автомат с тривиальным выходным алфавитом, то есть просто Состояния автомата (кроме ) – элементы Автомат работает корректно, если не существует способа его работы, при котором он переходит за конечное число шагов в неудачное состояние.

Математическая модель Класс линейных неубывающих блок-схем: а) s=1 б) в)

Математическая модель Теорема. Существует машина Тьюринга, которая по заданной на двоичной ленте стандартным образом линейной неубывающей блок- схеме B выводит в конце работы 1 тогда и только тогда, когда соответствующий автомат = (B) работает корректно над классом параметров N. int main() { int i, k, n, *a; n = 10; a = (int*) malloc (n * sizeof(int)); for (i = 0; i < n; i++) { a[i] = 0; for (k = 0; k < i; k++) a[i] += a[k]; } return 0; }

START i < n k < i STOP i = 0 n=10 a[i]=i k= k=k+1 a[i]=a[i]+a[k] i=i+1 Математическая модель Данная блок-схема не является линейной неубывающей. X Q(i) : 0 i

Вывод достаточных условий корректности 1. Выделение линейной части из условия корректности и условий информационой базы. 2. Исследование системы линейных неравенств, получение условий, достаточных для вывода условия корректности. 3. Применение логического вывода с использованием уже полученных фактов на шаге 2.

Анализ эффективности работы алгоритма. Программа была запущена на нескольких примерах линейного программирования. Результаты ее работы приведены на диаграмме. 14% 3,4% 14% 3,4% 14% 6,8% Количество переполнений (от общего числа обращений) Количество ложных тревог (от общего числа обращений) Исходный вариант СИ- программы (работа в единственной функции) Добавлены вызовы функций, немного перестроен порядок исполнения Работа алгоритма без внутреннего механизма эквивалентных преобразований блок-схемы Ускорение работы в 20,2 раза Анализ устойчивости алгоритма к различным стилям написания программ

Заключение 1. Предложен новый подход к проблеме переполнения буферов, позволяющий на основе исходных текстов программ гарантированно выявлять некорректные обращения к памяти. 2. Создан прототип алгоритма, реализующего эти идеи. 3. Программа была успешно протестирована на нескольких примерах. Была проверена устойчивость работы алгоритма к различным стилям написания программ. 4. В дальнейшем предполагается расширение класса анализируемых программ, как в глубину, так и в ширину 5. Главная цель исследования : создать эффективный метод автоматизации отслеживания угрозы переполнения буферов на стадии разработки программы.