Абстрактная интерпретация: от теории решеток к выводам и астрее.

Рассмотрим две программы, которые проходят все написанные вами тесты. Одна из них корректна. В другой возникает ошибка деления на ноль, которая появляется только при одновременном поступлении определённой комбинации входных данных, комбинации, которую ваши тесты никогда не воспроизводят. Традиционное тестирование не может определить, какая из них какая. Абстрактная интерпретация может.

Абстрактная интерпретация — это математическая основа, которая позволяет инструментам статического анализа рассуждать обо всех возможных вариантах поведения программы без её выполнения. Именно эта техника лежит в основе алгоритма Infer компании Facebook, обнаруживающего ошибки нулевого указателя в больших масштабах, в основе анализатора Astrée, формально верифицирующего программное обеспечение управления полётами Airbus, и в основе каждого статического анализатора, заявляющего о своей корректности, — гарантии того, что если программа проходит анализ, она действительно свободна от проверяемого класса ошибок. Понимание принципа её работы объясняет, почему одни инструменты обнаруживают ошибки, которые другие пропускают, и почему эти гарантии сопряжены с определёнными компромиссами.

Что такое абстрактная интерпретация?

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

Слово «абстрактный» здесь не означает расплывчатый или концептуальный. Оно относится к конкретной математической операции: абстрагированию набора конкретных значений в более простое представление, которое сохраняет важные для вас свойства, отбрасывая при этом ненужные детали. Конкретное целочисленное значение, например, 42 В рамках абстракции анализа знаков это значение становится просто «положительным». Абстракция теряет информацию (вы больше не знаете точное значение), но приобретает управляемость (знак любого целого числа может быть одним из трех: положительным, отрицательным или равным нулю).

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

Абстрактная интерпретация против анализа AST против динамического анализа

Эти термины часто путают: в результатах поиска по этой статье встречается запрос "анализ AST-кода", и они описывают разные вещи.

Абстрактное синтаксическое дерево (AST) — это структура данных, представляющая грамматическую структуру исходного кода. Каждый компилятор и линтер строит такое дерево. Оно является основой для синтаксического анализа, инструментов рефакторинга и статического анализа на основе шаблонов. Анализ на основе AST находит шаблоны: код, соответствующий правилу (функция со слишком большим количеством параметров, строка SQL, построенная путем конкатенации), помечается. Он не анализирует значения или поведение во время выполнения.

Абстрактная интерпретация анализирует поведение программы во время выполнения, не запуская её. Она использует абстрактное синтаксическое дерево (AST) в качестве входных данных, но выходит далеко за его рамки: моделирует, как значения проходят через программу, какие диапазоны могут принимать переменные, может ли указатель быть нулевым в конкретном месте вызова, завершается ли цикл. Анализ AST — это сопоставление с образцом. Абстрактная интерпретация — это поведенческое рассуждение.

Большинство линтеров (ESLint, Checkstyle, Pylint) в основном основаны на абстрактном синтаксическом дереве (AST). Большинство инструментов формальной верификации (Infer, Astrée, Polyspace) используют абстрактную интерпретацию. Динамический анализ (запуск программы и наблюдение за фактическим поведением) обнаруживает только ошибки, вызванные конкретными входными данными. Абстрактная интерпретация обнаруживает ошибки во всех возможных входных данных, не запуская программу вообще.

Математические принципы статического анализа

Запрос «каковы математические принципы, лежащие в основе инструментов статического анализа» появляется непосредственно в результатах поиска. Вот простой ответ.

Абстрактная интерпретация основывается на трех математических структурах:

Решетки. Решетка — это частично упорядоченное множество, где каждая пара элементов имеет наименьшую верхнюю границу (соединение) и наибольшую нижнюю границу (пересечение). В статическом анализе решетка представляет собой абстрактную область определения, множество возможных абстрактных значений, упорядоченных по объему передаваемой ими информации. Для анализа знаков решетка выглядит следующим образом:

        ⊤ (unknown -- could be anything)
       / \
   pos   neg
       \ /
        0
        |
        ⊥ (unreachable -- no possible value)

Перемещение вверх по решетке означает потерю точности (уменьшение знаний). Перемещение вниз означает ее повышение (увеличение знаний). Верхний элемент ⊤ означает «мы ничего полезного не знаем». Нижний элемент ⊥ означает «это состояние недостижимо».

Связи Галуа. Связь Галуа — это формальное отношение между конкретной областью (фактическими значениями программы) и абстрактной областью (упрощенным представлением). Она состоит из двух функций: функции абстракции α, которая отображает конкретные значения в их абстрактное представление, и функции конкретизации γ, которая отображает абстрактные значения обратно в набор конкретных значений, которые они представляют.

Ключевое свойство: абстрактная область определения должна представлять собой безопасное приближение с запасом. γ(α(S)) ⊇ S Для каждого конкретного множества S. Абстракция может включать больше значений, чем фактически встречается, что и приводит к ложным срабатываниям, но она никогда не должна исключать значения, которые действительно встречаются. Исключение реальных значений означало бы пропуск реальных ошибок.

Итерация с фиксированной точкой. Для программ с циклами анализ должен продолжаться до достижения стабильного состояния. Для цикла типа:

c

int x = 0;
while (condition) {
    x = x + 1;
}

В первой итерации, x is {0}После одного цикла тела, x может быть {0, 1}После двух, {0, 1, 2}Этот набор постоянно растёт, он никогда не стабилизируется сам по себе. Решение заключается в следующем: расширение: оператор, который обеспечивает сходимость путем перехода к более широкому приближению (обычно) [0, +∞) (для интервального анализа). Затем в анализе используется уменьшение чтобы восстановить некоторую точность.

Именно вычисления с фиксированной точкой обеспечивают полноту абстрактной интерпретации на всех путях выполнения, включая циклы, и делают их вычислительно более затратными, чем простое сопоставление с образцом.

Абстрактные области: выбор того, что следует аппроксимировать

Абстрактная область определяет, что анализ может и чего не может обнаружить. Разные области отвечают на разные вопросы о поведении программы.

Абстрактная область	Что он отслеживает	Пример использования	Чего в нём не хватает
Анализ знаков	Независимо от того, являются ли значения положительными, отрицательными или равными нулю.	Деление на обнаружение нуля	Точные значения, условия переполнения
Интервальный анализ	Верхняя и нижняя границы числовых значений	Переполнение буфера, безопасность доступа к массиву.	Отношения между переменными
Восьмиугольный домен	Линейные зависимости между парами переменных	Более точное обнаружение переполнения	Нелинейные зависимости
Анализ указателей	Указатели могут быть нулевыми или иметь псевдонимы друг друга.	Разыменование нулевого значения, использование освобожденной памяти	Время жизни объекта, форма кучи
Анализ загрязнения	Происхождение ценностей из ненадежных источников	SQL-инъекции, обнаружение XSS	Неявные потоки через управление
Полиэдральная область	Произвольные ограничения линейной арифметики	Проверка ограничений цикла	Затраты на повышение производительности растут экспоненциально.

Компромисс между доменами всегда сводится к соотношению точности и производительности. Интервальный домен работает быстро и выявляет большинство численных ошибок. Полиэдральный домен гораздо точнее, но имеет экспоненциальную сложность по количеству переменных. Практические инструменты статического анализа выбирают домены, которые обеспечивают баланс между точностью и производительностью для целевого приложения: критически важные для безопасности встроенные системы могут позволить себе более медленный, но более точный анализ; линтеры, интегрированные в системы CI/CD, должны завершать работу за секунды.

Как три реальных инструмента используют абстрактную интерпретацию

Вместо того чтобы описывать теорию изолированно, конкретные инструменты позволяют наглядно увидеть ее применение.

Facebook Infer использует форму абстрактной интерпретации, называемую биабдукцией, для анализа Java, C, C++ и Objective-C на предмет разыменования нулевых указателей, утечек ресурсов и состояний гонки. Биабдукция автоматически обнаруживает предварительные и постусловия для функций, что позволяет проводить межпроцедурный анализ без необходимости ручного указания параметров. Infer работает в системах непрерывной интеграции (CI) в Facebook, Spotify, Mozilla и десятках других крупных организаций, поскольку он масштабируется до кодовых баз объемом в несколько миллионов строк, оставаясь при этом надежным для проверяемых им классов ошибок.

Astrée использует абстрактную интерпретацию с числовыми абстрактными областями для доказательства отсутствия ошибок во время выполнения в программах на языке C. Airbus использовал его для формальной проверки основного программного обеспечения управления полетом A380, доказав отсутствие ошибок во время выполнения во всей системе управления — гарантия, которую не могла бы обеспечить ни одна программа тестирования. Astrée не обнаруживает ложных отрицательных результатов для проверяемых классов ошибок, хотя может выдавать ложные срабатывания, требующие ручной проверки.

Polyspace (MathWorks) применяет абстрактную интерпретацию для встроенного кода на C и C++ в приложениях, критически важных с точки зрения безопасности. Она классифицирует каждую операцию как «зеленую» (доказуемо отсутствие ошибки), «красную» (определенно ошибка) или «оранжевую» (потенциальная ошибка, требующая проверки). Классификация «зеленая» является формальным доказательством: ни одно выполнение не может вызвать ошибку во время выполнения на данной операции.

Треугольник «Надежность-Точность-Производительность»

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

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

Точность означает мало ложных срабатываний: результаты соответствуют реальным проблемам, а не теоретическим, которые не могут возникнуть. Высокая точность требует более точных абстрактных областей и межпроцедурного анализа.

Производительность означает, что анализ завершается за полезное время. Более точный анализ обходится дороже. Доказательство отсутствия всех ошибок времени выполнения в коде объемом в миллион строк занимает часы; сканирование линтером занимает секунды.

Для разных задач требуются разные точки в этом треугольнике:

• IDE-линтинг и CI/CD: производительность на первом месте, точность на втором, надежность по желанию
• Сканирование безопасности: точность в первую очередь (снижает утомляемость разработчиков на оповещения), надежность важна для классов с высокой степенью серьезности.
• Сертификация для критически важных объектов безопасности: надежность на первом месте (нельзя пропустить реальные ошибки), производительность на втором, ложные срабатывания допустимы при ручной проверке.

Абстрактная интерпретация в разработке встроенных систем и систем, критически важных для безопасности.

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

Нет тестового комплекта для всех состояний. Автомобильный ЭБУ реагирует на тысячи комбинаций датчиков в режиме реального времени. Создание тестов для каждой комбинации невозможно. Абстрактная интерпретация охватывает все состояния одновременно.

Требования к сертификации. Стандарты DO-178C (аэрокосмическая отрасль), ISO 26262 (автомобильная промышленность) и IEC 62443 (промышленное управление) требуют демонстрации корректной работы программного обеспечения во всех условиях. Формальная верификация с использованием абстрактной интерпретации может удовлетворить это требование таким образом, как это не могут сделать отчеты о покрытии тестами.

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

Анализаторы Astrée и Polyspace созданы специально для этой цели. Их конструкция допускает высокий уровень ложноположительных результатов и медленный анализ в обмен на гарантию отсутствия ложноотрицательных результатов.

Ложные срабатывания и усугубляющаяся проблема

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

Ложные срабатывания возникают по двум причинам:

Избыточное приближение в абстрактной области. Если интервальная область следов x ∈ [0, 100]оно не может различать случаи, когда x На практике всегда меньше 50. Деление на x может быть помечено как потенциально приводящее к делению на ноль, даже если логика программы гарантирует это. x > 0Более точная область определения (отслеживание точного значения или ограничение, связывающее значения). x (перенос значения в другую переменную) позволил бы исключить ложноположительные результаты, но с большими вычислительными затратами.

Расширение. Оператор сходимости, который делает анализ циклов разрешимым, неизбежно приводит к потере информации. После расширения x от [0, 5] в [0, +∞)анализатор больше не знает, что x остается ограниченным. Если код проверяет assert(x < 1000) После завершения цикла это утверждение уже нельзя доказать, даже если на практике это так. x всегда остается значительно ниже 1000.

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

Как SMART TS XL Применяет статический анализ в масштабах предприятия.

SMART TS XL Компания работает в сфере, где абстрактная теория интерпретации встречается с корпоративной реальностью: кодовые базы, охватывающие множество языков, десятилетия разработки и организационные границы, которые делают формальную проверку каждой программы нецелесообразной.

Вместо того чтобы применять единую абстрактную предметную область ко всем программам, SMART TS XLАвтора статический анализ кода Объединяет методы структурного анализа, подходящие для каждого языка программирования в среде: COBOL, JCL, Java, Python, RPG, PL/I, SQL и современных стеков, обеспечивая одновременное получение качественных метрик, данных о зависимостях и результатов анализа безопасности по всему портфелю продуктов.

Возможность сопоставления зависимостей приложений применяет теоретико-графовый анализ к графу межъязыковых вызовов, определяя, как программы, наборы данных и потоки заданий связаны между собой, преодолевая языковые барьеры. Это тот вид анализа всей системы, который недоступен для инструментов, работающих с одним языком. Это структурное рассуждение на системном уровне: доказательство не свойств отдельных программ, а свойств того, как они связаны между собой.

Функция анализа воздействия применяет анализ достижимости к графу зависимостей: при наличии предлагаемого изменения в одном узле вычисляется множество всех узлов, достижимых из него. Это статический анализ вопроса «что будет затронуто?», на который отвечает структура кода, а не наблюдение во время выполнения или оценка человека.

Для команд, проводящих модернизация наследия программы, SMART TS XLСтруктурный анализ, используемый в данной работе, устраняет разрыв между формальными абстрактными инструментами интерпретации (которые являются специфичными для конкретного языка и требуют экспертных знаний для настройки) и практической необходимостью понимания того, что на самом деле делают большие, недокументированные, многоязычные устаревшие системы, что является необходимым условием для любой программы модернизации, которая не хочет обнаружить свои самые дорогостоящие сюрпризы в процессе выполнения.

Часто задаваемые вопросы

В чём разница между абстрактной интерпретацией и проверкой моделей? Оба метода являются формальными методами верификации программ. Абстрактная интерпретация аппроксимирует множество возможных состояний с запасом (корректно, но потенциально неточно). Проверка моделей исчерпывающе исследует пространство состояний (полно, но осуществимо только для конечных, ограниченных систем). Абстрактная интерпретация масштабируется до больших программ. Проверка моделей масштабируется до сложных свойств на меньших моделях. Они дополняют друг друга, а не конкурируют.

Предназначена ли абстрактная интерпретация только для критически важного с точки зрения безопасности программного обеспечения? Нет, хотя именно там она проявляет свою наиболее очевидную ценность. Infer работает в стандартных конвейерах CI/CD крупных технологических компаний, выявляя разыменования нулевых указателей и утечки ресурсов в повседневном коде на Java и C. Степень применяемой строгости — это выбор: полная корректность с формальными гарантиями на одном конце спектра, легковесный эвристический анализ на другом, а большинство практических инструментов находятся где-то посередине.

Может ли абстрактная интерпретация анализировать COBOL? Теория абстрактной интерпретации не зависит от языка программирования. Для её применения к COBOL требуется реализация абстрактных функций передачи для операций COBOL, арифметики полей PIC, операторов REDEFINES, имен условий уровня 88 и т. д. Универсальные инструменты абстрактной интерпретации (Infer, Astrée) не поддерживают COBOL. Корпоративные платформы структурного анализа, которые изначально понимают COBOL, применяют соответствующие методы статического анализа для поиска проблем качества, мертвого кода и архитектурных проблем в кодовых базах COBOL.