Тема: Применение двунаправленного исполнения для вывода индуктивных инвариантов в символьной виртуальной машине KLEE

Тестирование — одна из обязательных частей разработки программно­го обеспечения. Целью тестирования являются нахождение ошибок и кри­тических уязвимостей в коде, минимизация усилий и времени, затраченных на проверку надёжности, производительности программы, её соответствия стандартам, правилам и требованиям.
Важным шагом в развитии тестирования программного обеспечения яв­ляется автоматизация генерации тестов, позволяющая освободить разработ­чиков от одной из тяжёлых и трудоёмких частей производства продукта [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% случаев позво­лила вывести индуктивный инвариант, тем самым упростив символьной машине анализ программы. Однако в ситуациях, когда потенциальная лемма-инвариант не встречается в качестве инструкции, алгоритм не улучшает анализ кода.
Купить