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

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

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