Разработка статического анализатора на основе символьного исполнения

Введение 4
Постановка задачи 7
1. Обзор предметной области 8
1.1. Существующие решения 8
1.1.1 SpotBugs 8
1.1.2 Coverity 8
1.1.3 CodeQL 9
1.1.4 Infer 10
1.1.5 Выводы 10
1.2. Символьное исполнение 11
1.2.1 Описание алгоритма 11
1.2.2 Пример работы 12
1.3. UnitTestBot 15
1.3.1 Архитектура 15
1.3.2 Пример работы 17
1.4. Taint-анализ 20
1.4.1 Описание алгоритма 20
1.4.2 Пример работы 22
2. Создание отчёта по сгенерированным тестам 24
2.1. Формат SARIF 24
2.2. Извлечение информации из тестов 26
2.3. Пример работы 27
3. Плагин для IntelliJ IDEA 30
3.1. Детали реализации 30
3.2. Пример работы 31
4. Taint-анализ 33
4.1. Конфигурация 33
4.2. Детали реализации 36
4.2.1 Общие концепции 36
4.2.2 Модификация символьной машины 37
4.2.3 Модификация генератора кода 40
4.3. Пример работы 40
5. Тестирование и эксперименты 43
5.1. Тестирование taint-анализа 43
5.2. Запуск на реальных проектах 45
5.2.1 Tape 45
5.2.2 Fastjson 46
5.3. Запуск на задачах Codeforces 47
Заключение 50
Список литературы 51
Приложение 55
Купить

Сложно представить себе разработку программного обеспечения в со­временном мире без применения инструментов анализа кода. По мере того как программы становятся сложнее, возрастает и сложность их тестирова­ния, а значит возрастает и потребность в автоматизации поиска ошибок или дефектов. Одним из подходов к решению этой задачи является статический анализ.
Статический анализ — это анализ программного обеспечения, произ­водимый (в отличие от динамического анализа [1]) без реального выполнения исследуемых программ. Чаще всего анализ производится над исходным ко­дом продукта, хотя иногда задействуется и какой-нибудь вид объектного ко­да, например, байт-код языка программирования Java. Таким образом, методы статического анализа помогают найти ошибки в коде ещё на этапе компиля­ции, что значительно ускоряет разработку программ, снижая потраченное программистом время на отладку и тестирование.
В связи с высокой востребованностью темы автоматического обнару­жения дефектов в программах, на рынке существует огромное количество различных статических анализаторов. Список из наиболее известных инстру­ментов, позволяющих анализировать Java код включает в себя SpotBugs [2], Coverity [3], CodeQL [4], Infer [5], а также многие другие. Перечисленные инструменты неплохо справляются с поиском простых ошибок или опечаток, однако в большинстве своём, не выполняют глубокого исследования кода, то есть не обнаруживают редкие сценарии исполнения, приводящие к некор­ректному поведению программы. Кроме того, часто допускается большое ко­личество ложноположительных срабатываний. Другими словами, инструмент может выдать предупреждение о найденной ошибке, которой на самом деле не существует. Это, конечно же, негативно сказывается на производительно­сти программиста, который теперь вынужден тратить время на рассмотрение выданного предупреждения.
Таким образом, существует запрос на разработку инструмента, который бы выполнял глубокий анализ и находил серьезные проблемы в коде, приводя­щие к неожиданному поведению программы. В достижении этой цели может помочь символьное исполнение.
Техника символьного исполнения заключается в том, чтобы исполнять программу не на конкретных значениях входных данных, а на так называе­мых символьных переменных. Благодаря этому, для каждого пути исполнения можно получить логические ограничения на значения входных параметров, при выполнении которых этот путь достигается. После этого при помощи SMT1-решателя такие значения могут быть найдены, и сгенерирован тесто­вый случай, реализующий данный путь. Описанный механизм обладает таким свойством, как теоретически полное покрытие кода, что позволяет обнаружи­вать редкие сценарии исполнения, которые приводят к неправильному резуль­тату работы программы. Ещё одно немаловажное достоинство символьного исполнения заключается в сравнительно небольшом количестве ложных сра­батываний относительно других методов статического анализа [6].
Для оценки качества анализатора кода обычно используется реестр са­мых опасных уязвимостей программного обеспечения [7]. Список включает в себя такие ошибки как запись или чтение вне границ массива, SQL-инъекция, использование непроверенного пользовательского ввода, разыменование ну­левого указателя, а также многие другие уязвимости, позволяющие злоумыш­ленникам полностью захватить систему, украсть данные или помешать работе приложений. Символьное исполнение способно находить далеко не все из пе­речисленных ошибок, однако его возможности могут быть существенно рас­ширены с помощью метода taint-анализа. Метод заключается в отслеживании распространения непроверенных внешних данных по программе и позволяет обнаруживать нарушения в безопасности, например, инъекции в базу данных, операционную или файловую систему. Таким образом, если встроить taint- анализ непосредственно в ядро символьной виртуальной машины, то можно объединить достоинства каждого из подходов, а именно, получить анализа­тор с низким уровнем ложноположительных срабатываний, который, помимо всего прочего, умеет находить проблемы в безопасности.
В рамках данной работы в качестве символьной виртуальной машины был взят UnitTestBot [8] — инструмент, который по исходному коду на языке Java автоматически генерирует тесты, пытаясь максимизировать покрытие. UnitTestBot может также находить тестовые случаи, приводящие к таким де­фектам в программном обеспечении, как выбрасывание необработанного ис­ключения, переполнения примитивных численных типов, зависания методов и некоторые другие. Однако сами по себе найденные значения входных па­раметров тестируемой функции ещё не являются приемлемым результатом статического анализа, поскольку качество анализатора измеряется не только в его способности находить неочевидные сценарии исполнения, но и в удобстве использования для программиста. Следовательно, выдаваемое предупрежде­ние о найденной ошибке, помимо краткого описания самой ошибки, должно содержать конкретное место в коде, а так же всю ту информацию, которая может помочь пользователю разобраться в проблеме как можно быстрее.
Немаловажным фактором удобства использования инструмента явля­ется простота его установки и запуска. В современном мире большинство программистов используют интегрированные среды разработки (англ. IDE), которые дают возможность встраивать в себя сторонние модули для реше­ния каких-либо задач. Например, UnitTestBot имеет собственный плагин для IntelliJ IDEA [9] — одной из наиболее популярных IDE для языка Java. В связи с этим было решено добавить функциональность выполнения стати­ческого анализа, а также отображения его результатов непосредственно в плагин UnitTestBot.
Купить