Суть спора: два подхода к формальной верификации

Формальные методы — это инструменты, позволяющие строго доказать соответствие системы (программы, протокола, микросхемы) поставленным требованиям. Однако два главных подхода верификации — модельная проверка и доказательство теорем — заметно различаются по предпосылкам, ресурсоёмкости и глубине гарантии.

Верификация теорем (Theorem Proving) строится на логических исчислениях и математических доказательствах. Специалист формулирует свойства системы как теоремы и доказывает их (вручную или полуавтоматически с помощью интерактивного доказателя — например, Coq, Isabelle, ACL2). Система абстрагируется как математическая модель. Такой подход позволяет получить абсолютное доказательство корректности относительно спецификации для всех входных данных, но требует больших интеллектуальных ресурсов и времени.

Проверка моделей (Model Checking) гораздо более автоматизирована. Ей дают конечную модель (например, в виде автомата) и свойства на языке темпоральной логики. Далее алгоритм сам проверяет модель на выполнение свойств — либо выдаёт подтверждение, либо выявляет контрпример. Однако анализируется не реальная система, а построенная модель; гарантия корректности даётся только для неё.

Таким образом, модельная проверка ищет ошибки в модели, а доказательство теорем строит строгое основание того, что ошибок нет в спецификации.

Как работает проверка моделей

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

Построение модели: система описывается понятным для инструмента языком (например, Promela для SPIN или временные автоматы для UPPAAL).
Формулировка свойств: требования оформлены формальным языком, обычно с помощью темпоральной логики (LTL, CTL): «по каждому запросу доступ предоставляется», «зелёный и красный не горят одновременно» и т.д.
Автоматический перебор: алгоритм строит пространство состояний и проверяет каждое на предмет нарушения свойств.

Главное ограничение — комбинаторный взрыв (экспоненциальный рост числа состояний в сложных системах). Для борьбы с этим используют абстракции и оптимизации.

[ИЗОБРАЖЕНИЕ: Диаграмма переходов состояний конечного автомата с проверкой свойства LTL]

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

Принципы верификации теорем

Здесь система и её спецификация описываются внутри выбранной логической теории: теория множеств, лямбда-исчисление, индуктивные типы и т.п. Наиболее распространены Coq, Isabelle/HOL и схожие средства.

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

Например, при доказательстве корректности сортировки потребуется формализовать и свойства «отсортированности», и понятие «перестановки», и вести индукцию по структуре программы.

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

Сравнение подходов

Критерий	Проверка моделей (Model Checking)	Верификация теорем (Theorem Proving)
Уровень гарантии	Для конкретной конечной модели. Возможны ошибки в абстракции.	Абсолютная математическая гарантия для спецификации.
Автоматизация	Полная автоматизация проверки.	В основном ручное, автоматизирована проверка шагов.
Результат при ошибке	Конкретный контрпример (сценарий нарушения).	Описание неудачного шага доказательства без подробного сценария.
Масштабируемость	Ограничена экспоненциальным ростом состояний.	Ограничена сложностью доказательства для человека.
Обучение и порог входа	Достаточно знать моделирование и базовую логику.	Необходимы глубокие знания логики, теории типов и доказательств.
Типичные применения	Протоколы, конечные автоматы, аппаратные контроллеры, анализ состояний.	Алгоритмы, криптографические протоколы, компиляторы, микроядра.

Когда стоит выбирать проверку моделей

Система конечна или легко сводится к конечной модели (контроллеры, автоматизация).
Нужен быстрый поиск ошибок и анализ сценариев.
Группа не готова вкладываться в полноценную формализацию.
Проверяются инварианты или отсутствие deadlock/livelock.

Когда актуальна верификация теорем

Максимальные гарантии — жизненно важные/криптографические системы.
Система оперирует бесконечными доменами (числа, динамические структуры).
Необходимы доказательства общей корректности алгоритмов.
Есть ресурсы и возможности для глубокой формализации.

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

Специфика российского регулирования

В отечественной нормативке (ФСТЭК, 152-ФЗ, ГОСТ) формальные методы обычно упоминаются как элемент повышения доверия к средствам защиты, но не конкретизируют инструментальные требования. При этом система оценки построена на результатах: важнее, чтобы риски снижены, а система надёжна, чем способ проверки.

Частая ошибка: использовать проверку моделей там, где она неадекватна задаче (например, проверять конечной моделью криптопротокол с бесконечным пространством сообщений и ключей). Гарантии распространяются только на исследованную модель, что не соответствует требованиям стандарта по СКЗИ. В этих случаях требуется именно верификация на уровне теорем для доказательства свойств на любом входе.

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

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

ГОСТ Р и профильные стандарты требуют, чтобы способ формального анализа соответствовал классу защищённости и был обоснован с точки зрения рисков, а не только «формально» выполнял требования.

Типовые сценарии выбора

Контроллер лифта или стрелки: конечный автомат, основные риски — deadlock и некорректные переходы. Проверка моделей эффективна, UPPAAL подходит для темпоральных свойств.
Криптографический модуль (СКЗИ): алгоритмы с бесконечным пространством входов и ключей. Верификация теорем: корректность должна быть доказана для любого input (EasyCrypt, VeriFast).
Ядро гипервизора: сложное взаимодействие, изоляция и синхронизация. Комбинированный подход: модельная проверка для протоколов и планировщика, глубокая верификация — для механизмов защиты.

Эти примеры иллюстрируют: ключ к выбору — структура задачи и требуемый уровень гарантий, а не личные предпочтения или «мода» на инструмент.

Скрытые сложности обоих методов

Вне зависимости от выбранной технологии остаются общие и уникальные ограничения.

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

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

Практические шаги для инженерной команды

Анализ системы: является ли система по сути конечной? Что критично — корректность алгоритма (функциональность) или только отсутствие deadlock/invariant?
Пилот: начните с малого модуля (аутентификация, простой контроллер) и проверьте оба подхода в простейших условиях.
Экспертиза и инструменты: оцените компетенции команды; используйте доступные инструменты — для моделей (SPIN, UPPAAL, TLA+), для теорем (Coq, Isabelle и пр.). При необходимости привлекайте сторонних специалистов.
Интеграция в разработку: формальные методы должны применяться параллельно проектированию, а проверки — автоматизироваться в CI/CD.
Документирование для регуляторов: обоснуйте выбраный путь, опишите ограничения и предположения модели, включите отчёты и выводы инструмента.

Формальные методы — это специализированные, мощные инструменты для риск-ориентированной разработки защищённых систем. Их эффективность определяется реальным пониманием границ метода: где достаточно анализа модели, а где строго необходимы формальные доказательства.