Введение 3
Постановка задачи 5
1. Обзор предметной области 6
1.1. Taint анализ 6
1.2. Символьное исполнение в KLEE 7
1.2.1 Генерация моков 9
1.3. Taint конфигурации 10
1.4. Существующие решения 11
2. Реализация taint анализа в символьной машине KLEE 13
2.1. Основная идея 13
2.2. Работа с памятью 13
2.2.1 Символьные taint выражения 14
2.2.2 Хранение в памяти символьных taint выражений .... 15
2.2.3 Чтение и запись в память символьных taint выражений . 15
2.3. Вспомогательные функции 16
2.4. Taint конфигурации 17
2.4.1 Taint правила 18
2.4.2 Аннотации функций 19
2.5. Генерация моков внешних функций 19
2.5.1 Загрязнение данных 20
2.5.2 Распространение загрязненных данных 20
2.5.3 Проверка загрязненности данных в стоке 20
2.6. Архитектура итогового решения 22
3. Эксперименты 23
3.1. Тестовый стенд 23
3.2. Результаты экспериментов 23
Заключение 25
Список литературы 26
В современном мире важной характеристикой любого программного продукта является его надежность, поскольку с ростом кодовой базы растёт вероятность появления в коде уязвимостей и ошибок. Поэтому тестирование является важнейшей и неотъемлемой частью разработки любого программного продукта. Но с увеличением объема кода растут затраты на тестирование, поэтому важной задачей является автоматизация тестирования и поиска уязвимостей. Одним из эффективных подходов для автоматизации тестирования является символьное исполнение [1]. Вместо конкретных данных, поданных на вход программы, символьное исполнение оперирует символьными выражениями, которые подразумевают под собой произвольные значения. Из ограничений на символьные выражения составляются предикаты, описывающие условия прохождения исследуемой программы по конкретному пути исполнения. Из модели условия пути можно получить конкретные входные данные, то есть тест, который приведёт к воспроизведению конкретной трассы. Так при помощи символьного исполнения можно получать тесты, воспроизводящие конкретные дефекты в программе. Это эффективный метод, который позволяет обнаружить маловероятные ошибки [1]. Одним из инструментов, реализующих символьное исполнение для компилируемых в LLVM [2] языков, является символьная виртуальная машина KLEE [3], которая используется в современных анализаторах кода, таких как KLOVER [4] и LibKluzzer [5].
Недостатком символьного исполнения является сложность анализа внешних функций, по путям исполнения которых не может пройти символьное исполнение [6]. Одним из решений данной проблемы является генерация моков для вызываемых в программе внешних функций [7]. Этот подход позволяет символьному исполнению продолжать обходить пути исполнения, несмотря на отсутствие доступа к настоящему телу внешней функции. Однако моки- рование не решает эту проблему полностью, поскольку неизвестно реальное поведение внешних функций, такие как их влияние на поступившие на вход данные, а также свойства возвращаемого значения. Вызовы функций, взаимодействующих с внешним окружением: файлами, сетью, библиотеками, — могут оказывать влияние на данные, задействованные в исследуемой программе, и приводить к ошибкам и уязвимостям. Примером подобной уязвимости является SQL-инъекция [8].
Одним из подходов для решения данной проблемы является taint анализ [9][10]. Основная идея этого подхода состоит в отслеживании распространения по программе потенциально опасных данных, полученных из внешнего источника, и нахождении путей их попадания в уязвимые места программы. В рамках данного подхода потенциально опасные данные, полученных из внешнего источника маркируются, а перемещение маркированных данных по программе отслеживается. Если маркированные данные не очищаются, то taint анализ сообщает об ошибке в случае их попадания в уязвимое место программы. Таким образом, задачей данной работы стала реализация taint анализа на базе символьного исполнения.
Основная идея реализации taint анализа при помощи символьного исполнения состоит в том, чтобы хранить символьную информацию о загрязненности объекта вместе с его символьным значением, использовать её при построении условий путей исполнения и таким образом отслеживать, существуют ли входные данные, при исполнении которых загрязненные данные дойдут от источника к стоку.
Подход был реализован в KLEE. Работа выполнена при поддержке российского исследовательского института Huawei. Тестирование реализованного инструмента проведено на тестовом наборе данных Juliet Test Suite for C/C++ 1.3. В результате тестирования на CWE134, на тестах, поддерживаемых текущим конфигурационным файлом аннотаций, было получено правдиво положительное значение на всех 195 тестах.
В данной работе были выполнены следующие задачи.
• Изучены существующие подходы к taint анализу, в том числе реализованные на базе символьного исполнения. В результате анализа информации были приняты решения относительно харнения и передачи загрязненных данных в символьном исполнении KLEE.
• Предложен и реализован способ хранения в символьной памяти и передачи во время исполнения загрязненных данных. Также были реализованы методы для работы с загрязненными данными в символьной памяти.
• Предложены и реализованы конфигурации для taint аннотаций и taint правил. Конфигурации являются полностью расширяемыми и независимыми.
• Реализована генерация LLVM кода для обработки taint аннотаций. Также были реализованы вспомогательные LLVM функции для работы символьной памятью в процессе исполнения.
• Проведено ручное тестирование на простых тестах. Проведено тестирование реализованного инструмента на тестовом наборе данных Juliet Test Suite for C/C++ 1.35.
Таким образом был разработано усовершенствование для символьной машины KLEE, использующее taint анализ с помощью символьного исполнения.
5https://github.com/arichardson/juliet-test-suite-c
