Ответ — нет. Настоящий вопрос в том, что оно может доказать взамен.

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

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

Почему тестирование миллиона сценариев всё равно оставляет вас в неведении

Типичная система управления полётом содержит сотни тысяч строк кода на C. Пространство входных данных — это декартово произведение показаний датчиков, команд пилота, условий окружающей среды и внутренних переменных состояния. Можно гонять систему в симуляторе до тепловой смерти Вселенной — и всё равно не покрыть каждый путь.

Тестирование находит ошибки. Оно не доказывает их отсутствие. Каждый пройденный тест — это лишь точка данных. Это не гарантия.

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

Конкретные значения слишком дороги. Используйте формы.

Рассмотрим простую переменную x. При конкретном выполнении x может быть равна 42. При абстрактной интерпретации x может быть «любое целое число от 0 до 255». Это называется интервальной абстракцией.

Анализатор отслеживает эти интервалы через каждую операцию. Если x — [0, 100], а y — [1, 10], то x / y — [0, 100]. Анализатор знает, что деление безопасно, потому что интервал делителя не включает ноль.

Но если бы y был [-5, 5], анализатор выдал бы предупреждение о возможном делении на ноль. Он не знает, попадёт ли конкретное выполнение на ноль. Он знает, что ноль лежит внутри возможного диапазона. Этого достаточно, чтобы поднять тревогу.

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

Соберём игрушечный интервальный анализатор на Python

Вот рабочий интервальный абстрактный домен. Он наивен, но демонстрирует механику.

from dataclasses import dataclass
from typing import Optional

@dataclass(frozen=True)
class Interval:
    lo: int
    hi: int

    def __post_init__(self):
        if self.lo > self.hi:
            raise ValueError("Empty interval")

    def add(self, other: "Interval") -> "Interval":
        return Interval(self.lo + other.lo, self.hi + other.hi)

    def div(self, other: "Interval") -> Optional["Interval"]:
        if other.lo <= 0 <= other.hi:
            return None  # Potential division by zero
        # Simplified: assumes positive divisor for demo
        return Interval(self.lo // other.hi, self.hi // other.lo)

    def intersect(self, other: "Interval") -> Optional["Interval"]:
        lo = max(self.lo, other.lo)
        hi = min(self.hi, other.hi)
        if lo > hi:
            return None
        return Interval(lo, hi)

    def __repr__(self):
        return f"[{self.lo}, {self.hi}]"


def analyze_division(a: Interval, b: Interval) -> None:
    result = a.div(b)
    if result is None:
        print(f"ALERT: {a} / {b} may divide by zero")
    else:
        print(f"SAFE: {a} / {b} = {result}")

Запустим несколько случаев:

analyze_division(Interval(10, 20), Interval(2, 5))   # SAFE
analyze_division(Interval(10, 20), Interval(-1, 1))  # ALERT
analyze_division(Interval(10, 20), Interval(0, 5))   # ALERT

Первый случай безопасен, потому что каждый делитель положителен. Второй отмечен, потому что ноль лежит внутри [-1, 1]. Третий отмечен, потому что ноль лежит внутри [0, 5].

Обратите внимание, что произошло в третьем случае. Конкретная программа может никогда не выполняться с b = 0. Анализатор этого не знает. Он консервативен по замыслу. Это фундаментальный компромисс.

Налог на ложные срабатывания

Корректный статический анализатор никогда не пропускает ошибку. Если сбой возможен, он сообщит о нём. Но он также сообщит о сбоях, которые невозможны. Эти ложные срабатывания — цена корректности.

На практике эта цена высока. Наивный интервальный анализ цикла вроде for (i = 0; i < n; i++) часто приходит к выводу, что i — [0, +∞], даже если n ограничен. Анализатор теряет точность в точках слияния, где соединяются два пути управления и их абстрактные состояния должны быть объединены.

Реальные инструменты используют более сложные домены. Полиэдры, октаэдры и предикатные абстракции отслеживают отношения между переменными. x < y невидимо для интервалов, но полиэдральный домен запоминает его. Эти домены точнее. Но и дороже. Полиэдральный домен имеет экспоненциальную сложность в худшем случае. Для системы управления полётом на 300 000 строк кода на C наивная реализация не завершится раньше вывода самолёта из эксплуатации.

Что Astrée действительно доказала на A380

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

Он не доказал, что самолёт не разобьётся. Он не доказал, что законы управления корректны. Он не доказал, что расчёт угла атаки соответствует физике самолёта. Это другие задачи, решаемые другими инструментами.

Astrée доказал, что программное обеспечение не уничтожит само себя. Это утверждение уже́, чем кажется, и ценнее, чем думает большинство. Самоуничтожение программ — частая причина авиационных катастроф. Доказать, что оно невозможно, стоит затраченных усилий.

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

Корректность — это выбор, а не умолчание

Не каждый статический анализатор стремится к корректности. Инструменты вроде Coverity, CodeQL и Infer отдают приоритет поиску реальных ошибок перед доказательством отсутствия. Они недоаппроксимируют пространство состояний. Могут пропустить деление на ноль, но те, что находят, обычно реальны.

Это законный инженерный выбор. Для веб-приложения искатель ошибок с точностью 90%, работающий за минуты, лучше корректного анализатора, который утопит вас в ложных срабатываниях. Для системы управления полётом — наоборот. Вы хотите доказательство, даже если придётся фильтровать шум.

Абстрактная интерпретация — это технология, делающая доказательство возможным. Это не единственный формальный метод. Верификаторы конечных автоматов вроде SPIN и TLA+ проверяют машины состояний. Теоремопруверы вроде Coq и Isabelle верифицируют функциональную корректность. Абстрактная интерпретация занимает золотую середину: она полностью автоматическая, масштабируется на большие codebases и даёт математические гарантии о поведении во время выполнения.

Где абстрактная интерпретация даёт сбой

У метода есть жёсткие ограничения. Он не может рассуждать о памяти, выделенной через сложную арифметику указателей. Он не может верифицировать, что алгоритм вычисляет правильное значение, — только то, что он не падает при вычислении. Он испытывает трудности с параллелизмом, динамической диспетчеризацией и кодом, который преднамеренно опирается на неопределённое поведение.

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

Начните с интервалов на реальной функции

Вам не нужен Astrée, чтобы применить эти идеи. Выберите одну чистую функцию в вашей кодовой базе. Определите одну переменную, которая должна оставаться в пределах. Напишите простой скрипт распространения интервалов. Отслеживайте переменную через каждую ветвь и операцию.

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

Абстрактная интерпретация не докажет, что ваш самолёт не разобьётся. Ничто не может. Но она может доказать, что ваше программное обеспечение не станет причиной этого.

FAQ

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

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

Может ли абстрактная интерпретация найти все ошибки?

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

В чём разница между корректным и некорректным статическим анализом?

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

Абстрактная интерпретация — только для критически важного ПО?

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