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

Сложно представить себе разработку программного обеспечения в со­временном мире без применения инструментов анализа кода. По мере того как программы становятся сложнее, возрастает и сложность их тестирова­ния, а значит возрастает и потребность в автоматизации поиска ошибок или дефектов. Одним из подходов к решению этой задачи является статический анализ.
Статический анализ — это анализ программного обеспечения, произ­водимый (в отличие от динамического анализа [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.
Купить

Основным результатом работы является готовый к использованию ин­струмент статического анализа кода на языке Java. В процессе достижения этой цели были выполнены следующие задачи.
• Проведён обзор существующих на рынке решений, в ходе которого бы­ли выявлены их ключевые недостатки — поверхностность проводимого анализа, а также большое количество ложноположительных срабатыва­ний.
• Реализован модуль создания отчётов в формате SARIF на основе тесто­вых случаев, сгенерированных инструментом UnitTestBot.
• Разработан удобный пользовательский интерфейс для просмотра отчё­тов SARIF в среде разработки IntelliJ IDEA.
• В символьную виртуальную машину встроена техника taint-анализа, рас­ширяющая её возможности. Реализованный алгоритм позволяет нахо­дить нарушения безопасности, а именно, случаи использования непро­веренных данных в критических секциях программы.
• Разработанный статический анализатор был протестирован на несколь­ких известных проектах с открытым исходным кодом, а также на ре­шениях задач с сайта Codeforces. Проведённые эксперименты показали возможность применения продукта на практике.
Купить