Введение 3
Постановка задачи 5
1. Обзор предметной области 6
1.1. Символьное исполнение 6
1.2. Проблема анализа внешних вызовов с использованием символьного исполнения 9
1.3. Обзор существующих решений 11
1.4. Выводы 13
2. Архитектура символьной виртуальной машины KLEE 15
2.1. LLVM 15
2.2. Основные компоненты KLEE 15
2.2.1 Препроцессор 16
2.2.2 Интерпретатор 17
2.2.3 Конструктор запросов к Z3 18
2.3. Алгоритм воспроизведения тестов 18
3. Реализация алгоритма анализа внешних вызовов 19
3.1. Основная идея алгоритма 19
3.2. Стратегии изоляции 20
3.2.1 Недетерминированные символьные модели 20
3.2.2 Детерминированные символьные модели 20
3.2.3 Пример работы реализованных стратегий изоляции . . . 21
3.3. Реализация символьных моделей для аллокаторов 23
3.4. Архитектура итогового решения 24
4. Тестирование 26
4.1. Тестовая инфраструктура 26
4.2. Результаты 26
4.2.1 Недетерминированные символьные модели 26
4.2.2 Детерминированные символьные модели 29
4.3. Выводы 29
Заключение 31
Список литературы 32
Важнейшей характеристикой любого программного продукта является его надёжность. Именно поэтому тестирование — неотъемлемая часть разработки программного обеспечения. Автоматизация процесса тестирования позволяет значительно снизить стоимость разработки компьютерных программ [1]. Одним из распространённых методов автоматической верификации программного обеспечения является символьное исполнение [2].
Идея классического символьного исполнения состоит в выполнении программного кода таким образом, что вместо конкретных данных на вход программа получает символы, представляющие собой произвольные значения. Такой подход позволяет анализировать даже очень редкие сценарии поведения, чего трудно добиться, используя случайное тестирование.
Одной из проблем, с которой сталкивается символьное исполнение, является анализ взаимодействия программы с внешним окружением [3]. Работа с системными вызовами, сторонними библиотеками, файлами, сетью и другими внешними объектами часто приводит к побочным эффектам, которые крайне трудно исследовать в тех случаях, когда параметры взаимодействия являются символьными.
В основном современные символьные виртуальные машины решают эту задачу, создавая собственные модели для часто используемых стандартных функций и явно вызывая остальные внешние функции с конкретными аргументами. Несмотря на то, что такой подход демонстрирует хорошие результаты при тестировании небольших проектов, он имеет ряд недостатков при работе с промышленным кодом.
Во-первых, таким образом не получится анализировать пользовательские внешние функции, которые невозможно исполнить явно в момент тестирования. Такие ситуации часто возникают в процессе промышленной разработки в силу того, что над кодом программного продукта могут параллельно работать несколько команд. Так, исследование компании Microsoft [4], направленное на изучение инструментов и рабочих привычек сотрудников компании, показало, что 54% опрошенных используют модульное тестирование с целью упрощения взаимодействия между командами.
Во-вторых, конкретизация символьных аргументов перед вызовом внешней функции может приводить к потере некоторых ветвей исполнения, а следовательно, и к пропуску критических уязвимостей. Возможность анализа каждой из достижимых инструкций является важным свойством символьного исполнения, на которое опираются многие приложения [5].
В-третьих, конкретное исполнение внешних вызовов в ходе анализа программы затрудняет воспроизводимость сгенерированных тестов, так как они могут вести себя по-разному в зависимости от внешних условий. Например, если в ходе выполнения теста вызывается функция, возвращающая текущее время, то результат может зависеть от времени на машине, где проводится тестирование. Такие нестабильные тесты негативно влияют на эффективность и надёжность процесса верификации [6].
Таким образом, для внедрения техники символьного исполнения в процессы тестирования программного обеспечения в IT-компаниях необходимо преодолеть упомянутые выше трудности. Данная работа решает эту задачу путём усовершенствования символьной виртуальной машины KLEE [7], которая занимает высокие позиции в соревнованиях по автоматическому тестированию [8], [9], [10] и лежит в основе многих современных инструментов анализа кода, таких как TracerX [11], Symbiotic 8 [12], KLOVER [13], Cloud9 [14], LibKluzzer [15] и многих других.
Работа выполнена при поддержке российского исследовательского института Huawei. Кодовая база компании Huawei насчитывает гигабайты исходного кода на языках C и C++. Для упрощения тестирования такие большие проекты разделяют на модули, тестируемые в отдельности. Отсюда возникает большое количество внешних вызовов. Поэтому данная работа имеет большое значение для процессов автоматизации тестирования компании.
В данной работе были выполнены следующие задачи.
• Рассмотрены способы анализа внешних вызовов, реализованные в различных инструментах символьного исполнения. В результате проведённого обзора было принято решение реализовать автоматическую изоляцию тестируемого кода при помощи генерации символьных моделей для внешних функций. В качестве основы для реализации алгоритма была выбрана символьная виртуальная машина KLEE.
• Разработаны два типа символьных моделей: детерминированные и недетерминированные. Их использование позволяет пользователю получать более релевантные его запросу тесты.
• Разработан и реализован алгоритм автоматической генерации символьных моделей для внешних функций. Также реализован механизм воспроизведения тестов, содержащих внешние вызовы, с использованием сгенерированных символьных моделей.
• Разработаны и реализованы символьные модели для стандартных аллокаторов языка C. Также поддержано воспроизведение тестов, полученных в результате применения данных моделей. Данная функциональность позволяет анализировать редкие сценарии выполнения программы, а также детерминировано их воспроизводить.
• Проведена апробация реализованной функциональности на проекте FRRouting, которая показала эффективность модифицированного KLEE в сравнении с оригинальным в случае анализа программ, содержащих внешние вызовы. Модифицированному KLEE удалось покрыть 1700 из 4200 тестируемых строк кода, что составило 40%. В то же время оригинальный KLEE не покрыл ни строки в связи наличием в исходном коде внешних переменных.
