Принципы работы статического анализа кода

Статический анализ кода — это программный анализ кода программы без ее реального выполнения.

Сегодня статический анализ кода всё чаще используется при проверке свойств программного продукта, используемого в компьютерных системах высокой надёжности, например, программных продуктах для медицинских аппаратов, ядерных и тепловых станций, авиационной техники. Применяется он и в информационной безопасности при поиске кода, потенциально содержащего уязвимости. По данным VDC за 2012 год, 28% разработчиков встраиваемых программных продуктов уже активно используют средства статического анализа, и 39% собираются начать их использование в течение следующих двух лет. Чтобы понять, почему и зачем нужен статический анализ кода, в сегодняшней статье мы рассмотрим его базовые понятия и основополагающие принципы работы.

Проблема остановки — это проблема в теории алгоритмов, которая, формально говоря, задается вопросом завершится ли когда-нибудь выполнение определенной программы определенным исходом. Проблема эта неразрешима, то есть не существует общего алгоритма ее решения и не один алгоритм не может разрешить ее для всех программ и всех исходов. Кстати говоря, неразрешимость проблемы остановки — это одна из интереснейших и важнейших тем компьютерной науки. Таким образом, статический анализ — это такие алгоритмы, которые делают все возможное, чтобы противостоять неразрешимости проблемы остановки, другими словами эти алгоритмы пытаются предсказать поведение программы. Предсказание поведения программы способствует ее оптимизации, позволяет сделать аудит безопасности и даже проверку корректности.

Проблема остановки создает сложности в выявлении причин поведения программы. Например, предположим, что вы хотите знать, будет ли программа выдавать ошибку несоответствия размерам массива для следующего выражения:

a[i]

Во-первых, зацикливаем все возможные точки исхода программы — программа гарантированно не будет завершена. Затем меняем индексирующее выражение на:

((i >= 0 && i < a.length) ? a[i] : exit())

Если у нас получается разрешить проблему остановки, то мы можем использовать это для проверки ошибок границ массива.

Предположим и другой вариант: у нас есть специальная программа, которая может определить наличие ошибок границ массива. Сделаем те же самые преобразования для индексирующих выражений, что и выше. Это устранит все ошибки программы, связанные с границами массива, через трансформацию их к завершению. Теперь изменим каждую оригинальную точку исхода в ясную ошибку, связанную с границами массива, т. е. a[a.length+10]. Если проверка на ошибки границ массива покажет ошибки выхода за границы, то это однозначно скажет о том, что изначальная программа останавливается, а если проверка не выдает таких ошибок — то изначальная программа не останавливается. Другими словами, если мы можем найти ошибки границ массива, то мы можем решить проблему остановки.

Ключевой принцип статистического анализа — это обеспечение приближенной интерпретации абстракции программы. Во многих случаях эти абстракции имеют предел и гарантируют завершение приближенной интерпретации.

Например, возьмем простой регистровый машинный язык. Чтобы проанализировать программы на этом языке, сначала нам нужна конкретная семантика — интерпретер, который избегает использование эффектов. Почему? Потому что, когда программа избегает использование эффектов, она больше не является программой, а является математическим артефактом, из которого мы можем извлечь и доказать корректность статического анализа кода. Определим теперь значение выражений: нам нужна функция, чтобы мы сопоставили выражение с его значением. Карта таких сопоставлений в коде будет представлена в виде карты с постоянными хэшами. Далее определяются состояния машины, а затем значение состояний. Анализатор простого регистрового языка будет имитировать интепретера, но здесь мы заменим целые значения на абстрактные — для этого будет полезно определять абстракцию в коде. Абстрактные состояния имеют ту же структуру, что и конкретные состояния. Таким образом, в конце анализа у вас будет коллекция посещенных состояний. Для данного состояния s и данной переменной v можно найти абстрактное состояние в s и затем отыскать v в ее среде, чтобы найти ее возможные знаки. На практике даже от такого простого анализа всегда будет польза.

P.S. По мере добавления нового функционала к языку у интерпретатора наращивается сложность. Наращивается, соответственно, и сложность анализатора. Исследования в статистическом анализе фокусируются на борьбе и использовании этого роста. И в качестве исследуемой области статистический анализ нацелен на анализ более богатых языков за меньшее время с более высокой точностью одновременно.

intro static analysis