Тестирование — одна из обязательных частей разработки программного обеспечения. Целью тестирования являются нахождение ошибок и критических уязвимостей в коде, минимизация усилий и времени, затраченных на проверку надёжности, производительности программы, её соответствия стандартам, правилам и требованиям.
Важным шагом в развитии тестирования программного обеспечения является автоматизация генерации тестов, позволяющая освободить разработчиков от одной из тяжёлых и трудоёмких частей производства продукта [1]. Основная проблема автоматизации тестирования состоит в том, что количество путей исполнения в программе может быть сколь угодно большим. Следовательно, автоматический генератор тестов должен создать столько входных аргументов для тестируемой функции, сколько необходимо для покрытия максимально возможного количества путей исполнения.
Современные подходы к решению этой проблемы являются комбинацией поведенческого (black-box test generation) и структурного (white-box test generation) тестирования [2]. Традиционным примером поведенческого тестирования является генерация случайных входных данных для программы (или же «фаззинг»), а структурного — символьное исполнение. Если сравнить поведенческое и структурное тестирование, то можно отметить, что поведенческое тестирование быстрее анализирует пути исполнения, однако обладает неточностью, поскольку не покрывает редкие, труднодостижимые пути. Наоборот, структурное тестирование отличается своей точностью, но работает медленнее, так как сталкивается с проблемой «взрыва числа путей исполнения» [3]. «Взрыв путей» происходит из-за того, что условные операторы и операторы цикла экспоненциально увеличивают количество возможных путей исполнения программы. На практике большая часть путей не представляет интереса для тестирования, поскольку не добавляет нового поведения в сравнении с уже проанализированными. Проблеме «экспоненциального взрыва» уделяется большое внимание со стороны научного сообщества [4, 5, 6].
Одним из возможных подходов структурного анализа является прямое символьное исследование кода программы, а именно символьное исполнение от точки входа. Но такой способ не может осуществить направленное исследование к конкретной инструкции в коде. В дополнение к прямому можно использовать обратное символьное исполнение, позволяющее запустить исследование в направлении от целевой инструкции к точке входа [7]. И в том, и в другом случае существует проблема анализа большого числа абстрактных путей, не реализующихся в реальности. Эффективной комбинацией этих двух подходов является двунаправленное символьное исполнение [8].
Двунаправленное исполнение может помочь в решении основной проблемы символьного исполнения — проблемы «взрыва путей». При анализе вопроса «экспоненциального взрыва» можно обнаружить, что не всегда различное количество итераций цикла будет приводить к отличающимся результатам работы программы. Существуют ситуации, в которых программа сохраняет свойство некоторого состояния вне зависимости от числа итераций цикла, другими словами, поддерживает инвариант. Инвариантами можно воспользоваться для уменьшения числа путей анализа программы, чтобы отбрасывать заведомо недостижимые участки кода.
Одним из популярных и широко используемых инструментов с открытым исходным кодом, который занимается автоматической генерацией тестов на основе символьного исполнения, является KLEE [9].
Данная работа посвящена улучшению анализа кода символьной виртуальной машиной KLEE путём внедрения вывода индуктивных инвариантов при помощи стратегии двунаправленного исполнения.
В данной работе были выполнены следующие задачи:
• Проведён обзор существующих подходов и решений в области вывода индуктивных инвариантов среди инструментов автоматической генерации тестов 2LS, Angr и KLEE. В ходе обзора в качестве основы для реализации алгоритма был выбран инструмент KLEE.
• Разработан эффективный алгоритм проверки лемм на индуктивность с применением двунаправленного символьного исполнения. Описаны необходимые модификации исходного алгоритма двунаправленного исполнения для внедрения возможности проверки лемм на индуктивность.
• Полученный алгоритм реализован в виртуальной символьной машине KLEE. Описаны необходимые структуры данных и детали реализации.
• Проведено тестирование реализации на проверочных данных соревнования SVComp. Модифицированная версия KLEE в 67% случаев позволила вывести индуктивный инвариант, тем самым упростив символьной машине анализ программы. Однако в ситуациях, когда потенциальная лемма-инвариант не встречается в качестве инструкции, алгоритм не улучшает анализ кода.
