Введение 5
1. Постановка задачи 7
2. Обзор предметной области 8
2.1. Символьное исполнение 8
2.2. SMT-решатели 11
2.3. Архитектура проекта V# 12
2.4. Модель символьной памяти в V# 13
3. Независимое управление ограничениями 15
3.1. Существующие реализации 16
3.2. Подход к реализации в V# 17
4. Кэширование моделей SMT-решателя 19
4.1. Существующие реализации 19
4.2. Подход к реализации в V# 21
5. Инкрементальное использование SMT-решателя 22
5.1. Инкрементальность на основе стека 23
5.2. Инкрементальность на основе предпосылок 24
5.3. Существующие реализации 26
5.4. Подход к реализации в V# 26
6. Особенности реализации 28
6.1. Независимое управление ограничениями 28
6.2. Кэширование моделей SMT-решателя 30
6.3. Инкрементальное использование SMT-решателя 31
7. Эксперименты 32
7.1. Тестовые данные 32
7.2. Исследовательские вопросы 32
7.3. Результаты 33
Заключение 37
Список литературы 38
Качественное тестирование достаточно сложной, чтобы быть полезной не только для ее создателя, программы — это, как правило, трудоёмкая задача. Тестирование требует значительного количества времени, которое не всегда удаётся выделить в реальном процессе разработки. При этом даже после тестирования и отладки в программном коде могут оставаться незамеченные специалистами уязвимости, приводящие к ошибкам или нежелательному поведению только при исполнении на специфичных комбинациях входных данных. Для решения данных проблем часто применяются инструменты автоматической генерации тестов, в том числе инструменты тестирования «белого ящика» (которым доступен исходный код программы, в отличие от тестирования «черного ящика»). В основе таких инструментов лежат различные механизмы статического анализа кода, один из которых — механизм символьного исполнения.
Техники символьного исполнения кода заключаются в исполнении программы не на конкретных значениях входных данных, а на так называемых символьных переменных. Это даёт возможность для каждого пути исполнения получить логические ограничения на значения входных параметров, при выполнении которых этот путь достигается. После этого при помощи БМТх-решателя такие значения могут быть найдены и сгенерирован тест, реализующий данный путь.
Механизм символьного исполнения обладает таким достоинством, как теоретически полное покрытие кода, что даёт возможность гарантировать выполнение некоторых условий программой (например, что она никогда не выбрасывает Null Pointer Exception). В то же время необходимость анализировать все возможные пути исполнения, число которых растет экспоненциально, влечёт его главный недостаток — высокую вычислительную сложность. К этому также следует добавить NP-трудность задачи выполнимости формулы в теориях, к которой, как правило, сводится задача поиска значений входных данных.
■Satisfiability Modulo Theory, задача выполнимости формулы в теориях
В качестве примера, иллюстрирующего эффективность и сложность символьного исполнения, можно привести использование компанией Microsoft символьной машины SAGE для воспроизведения ошибки переполнения стека в ОС Windows [15]. Ошибка в коде, отвечающем за чтение файлов анимированных курсоров, приводила к возможности удаленного исполнения произвольного кода злоумышленником1. В отличие от других инструментов статического анализа, SAGE удалось сгенерировать файл, чтение которого приводило к ошибке, но на это понадобилось семь с половиной часов на машине с производительностью среднего ПК.
Таким образом, создание практически полезного инструмента, основанного на механизме символьного исполнения, невозможно без использования различных оптимизаций и эвристик. Существует большое количество подходов к управлению ограничениями в символьных машинах, позволяющих минимизировать число запросов к SMT-решателю, увеличить переиспользование уже полученных в процессе исполнения результатов и исключить определённые пути исполнения.
V#2 — это символьная машина для программ на платформе .NET с открытым исходным кодом, которая разрабатывается с целью удовлетворить текущую потребность 3 в системе автоматической генерации тестов для наиболее современных фреймворков .NET и .NET Core, используя при этом наиболее современные подходы к оптимизации процесса символьного исполнения.
В ходе данной работы были получены следующие результаты.
• Проведён обзор оптимизаций управления символьными ограничениями: техник независимого управления ограничениями и кэширования моделей SMT-решателя, подходов к инкрементальному использованию SMT-решателя на основе стека и предпосылок.
• Независимое управление ограничениями реализовано в символьной виртуальной машине V#.
• Кэширование моделей SMT-решателя реализовано в символьной виртуальной машине V#.
• Подход к инкрементальному использованию SMT-решателя на основе предпосылок реализован в символьной виртуальной машине V#.
• Проведены эксперименты на синтетических тестовых данных.
Исходный код проекта V# является открытым и содержится в репозитории GitHub1 (имя аккаунта — mxprshn).
