Проектирование и разработка универсальной символьной виртуальной машины

Введение 4
Постановка задачи 6
1. Обзор предметной области 7
1.1. SMT-решатели 7
1.2. Символьное исполнение 9
1.3. Общее устройство символьной машины 11
1.4. Общие проблемы в символьном исполнении 12
1.5. Существующие символьные машины 15
2. Описание символьной виртуальной машины 17
2.1. Основные решения 17
2.2. Архитектура 18
2.3. Представление выражений 21
2.3.1 Библиотека KSMT 21
2.3.2 Представление примитивных значений 22
2.3.3 Представление ссылочных значений 23
2.3.4 Представление массивов 24
2.3.5 Представление символьных выражений программы 24
2.4. Символьное состояние 27
2.5. Символьная память 28
2.5.1 Регистровый стек 31
2.5.2 Хранилище типов 32
2.6. Символьная куча 32
2.6.1 URegionHeap и регионы памяти 34
2.6.2 Дерево регионов 38
2.6.3 Разделение символьных и конкретных адресов 44
2.7. Модель 48
2.7.1 Композиция 49
2.8. Решатель ограничений 53
2.8.1 Транслятор и декодер 53
2.8.2 Решатель типовых ограничений 54
2.9. Интерпретатор 56
2.10. Очередь состояний 57
2.11. Дополнительные детали 58
2.11.1 Список типов для объекта 58
2.11.2 Операции группового копирования 58
2.11.3 Моделирование библиотеки 59
2.11.4 Регионы типов 59
3. Полученные результаты 60
3.1. Практическое применение 60
3.1.1 Тестовый язык программирования 60
3.1.2 Java 61
3.2. Замеры производительности 62
3.2.1 Скорость работы кучи 62
3.2.2 Сравнение с UTBotJava 64
3.3. Дальнейший планы 66
Заключение 67
Благодарность 68
Список литературы 69
Купить

Количество инструментов для анализа кода, помогающих в цикле раз­работки и поддержки программного обеспечения, постоянно растёт. Область их применения действительно широка: поиск ошибок в процессе написания кода; валидация кода на соответствие стилю, принятому в команде; автомати­ческая генерация регрессионных тестов; автоматическое нахождение ошибок и уязвимостей; автоматическая проверка инвариантов программ; помощь в написании программ с заданными свойствами; поиск деградаций производи­тельности; генерация описаний функции и многое другое.
Одним из наиболее эффективных и точных подходов в анализе про­грамм является так называемое символьное исполнение. Анализаторы, осно­ванные на символьном исполнении, используются в системах непрерывной сборки в крупных компаниях, таких как Microsoft. Например, инструмент SAGE, использующий символьное исполнение, помог найти критическую ошибку в исходном коде операционной системы Windows [1]. Символьное исполнение активно используется для генерации модульных тестов, позволяя существенно повысить качество кода и сэкономить время разработчиков и тестировщиков.
Идея, лежащая в основе символьного исполнения, заключается в иссле­довании программы путём перебора различных путей исполнении и проверке предикатов, определяющих очередной путь. При этом конкретные входные значения программы заменяются на символьные, таким образом получается исчерпывающее описание условия ошибки, выраженное с помощью предика­тов на входные значения.
Одним из преимуществ символьного исполнения по сравнению с други­ми техниками является теоретическая доказуемость. Иначе говоря, с помо­щью символьного исполнения можно проверять некоторые свойства анализи­руемой программы. К основным недостаткам символьного исполнения можно отнести высокую вычислительную сложность, связанную с необходимостью исследования большого количества состояний программы. К тому же задача проверки выполнимости формулы в теории SMT1, на которой основан лю­бой алгоритм символьного исполнения, является NP-трудной2, и её решение может занимать длительное время.
Впервые идея символьного исполнения была представлена в статье 1976 года [2], однако наиболее активно развиваться и применяться символьные ма­шины начали только в конце XX-начале XXI века. Например, для языков, ком­пилирующихся в LLVM [3], появилась символьная машина KLEE [4], широко распространённая в индустрии и объединяющая большое количество иссле­дователей из академической среды. С другой стороны, для многих языков всё ещё не существует решения, удовлетворяющего ограничениям по точности и прежде всего масштабируемости.
Дополнительно стоит отметить, что многие символьные машины реа­лизуют похожие сущности, имеют общую архитектуру и решают одинаковые проблемы, независимо от анализируемого языка. Таким образом, возникает потребность в эффективной реализации ядра символьной машины, подходя­щего для различных целей. Идея данной работы заключается в выделении, проектировании и реализации некоторого набора компонентов, позволяюще­го реализовать эффективный символьную машину для любого целевого языка с автоматическим управлением памятью, такого как Java, Go, Python и т.д. Данное ограничение является довольно существенным, однако оно позво­ляет существенно оптимизировать представление памяти будущего ядра, к тому же согласно индексам популярности языков программирования TIOBE [5] и PYPL [6], языки с автоматическим управлением памятью составляют большую часть на рынке.
Постановка задачи
Целью данной работы является создание ядра универсальной символь­ной виртуальной машины, подходящей для анализа языков программирова­ния с автоматическим управлением памятью.
Для достижения поставленной цели были выделены следующие задачи:
• Анализ существующих символьных машин и различных техник в сим­вольном исполнении.
• Проектирование и разработка основных компонентов универсальной символьной виртуальной машины, подходящей для анализа языков с автоматическим управлением памятью.
• Реализация с использованием полученной машины анализатора для языков, компилирующихся в JVM байт-код, поддерживающего основ­ной набор инструкций.
• Замеры производительности полученного анализатора и сравнение с одним из существующих анализаторов для языка Java.
Купить