CVE-2026-72705 — Проверка guard checker в Rocq принимает Fixpoint, переданный как аргумент высшего порядка

Доказательство 0 = 1 без аксиом через парадокс Рассела посредством обхода fixpoint в guard checker.

Обнаружено автономно Claude Opus 4.6 (Anthropic).

Поле	Значение
Отчёт об ошибке	rocq-prover/rocq#21683
Исправление	PR #21684
Затронуто	Rocq ≤ 9.1.0 / все версии Coq с guard checker
Исправлено в	9.2.0
CVSS 3.1	`AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N` — 7.1
CWE	CWE-670 (Always-Incorrect Control Flow Implementation)
CVE	CVE-2026-72705

Краткое описание уязвимости

Guard checker принимает fixpoint, которые передают сами себя как аргументы высшего порядка другому fixpoint, который затем вызывает их на не-подтермах структурного аргумента. Передача рекурсивной функции в Definition (не-fixpoint константу) корректно отклоняется — guard checker разворачивает её и видит проблемный вызов. Но передача её в Fixpoint некорректно принимается.

Это создаёт парадокс в стиле Рассела в 4 строках:

Definition delta (x : russell 1) : False := x x.
Definition omega : False := delta delta.

где russell 1 по определению равен russell 1 -> False — тип, который является собственным отрицанием. Самоприменение напрямую даёт False.

Эксплойт:

Не использует никаких аксиом, плагинов или небезопасных возможностей
Print Assumptions сообщает "Closed under the global context"
Всё доказательство False — это 4 строки функционального кода
Никаких тактик, никакого Qed — чисто дефиниционально

Использование

docker build -t rocq-cve-poc-21683 .
docker run --rm rocq-cve-poc-21683

Влияние

Затронута любая система, которая доверяет проверенным ядром Rocq доказательствам:

Формально верифицированное программное обеспечение: CompCert, CertiKOS, Iris, MathComp
Смарт-контракты: ConCert, верифицированные DeFi
Доказательства, сгенерированные ИИ: любая система, использующая Rocq в качестве доверенного бэкенда

Технические подробности

Построение парадокса

iterate_to_neg f n seed :=
  match n with
  | 0   => f seed -> False      (* negate after n steps *)
  | S m => iterate_to_neg f m seed
  end

russell n :=
  match n with
  | 0   => True
  | S m => iterate_to_neg russell 1 (S m)   (* passes ITSELF *)
  end

Проверка защиты должна отклонить russell, поскольку он передаёт сам себя как аргумент высшего порядка в iterate_to_neg, который затем вызывает его на S m (не подтерм n). Но проверка отслеживает только прямые рекурсивные вызовы, а не вызовы через аргументы неподвижной точки высшего порядка.

Редукция

russell 1 = iterate_to_neg russell 1 1
          = iterate_to_neg russell 0 1
          = russell 1 -> False

Итак, russell 1 ≡ russell 1 -> False. Это классическое множество Рассела: множество всех множеств, которые не содержат сами себя. Самоприменение даёт:

delta : russell 1 -> False    (* russell 1 = russell 1 -> False *)
delta x := x x                (* x : russell 1 = russell 1 -> False *)

omega : False
omega := delta delta           (* delta : russell 1 -> False = russell 1 *)

Обнаружение

Эта ошибка была найдена автономно Claude Opus 4.6 во время ночного прогона фаззинга, организованного Tristan Stérin (@tcosmo), на основе указаний Yannick Forster (@yforster) о проверке guard. ИИ выявил паттерн обхода неподвижной точки высшего порядка и построил минимальный эксплойт iterate_to_neg/russell.

См.: ветка Zulip

Благодарности

Обнаружение ошибки: Claude Opus 4.6 (Anthropic), настройка — Tristan Stérin (@tcosmo)
Исправление ядра: PR #21684
Упаковка PoC: Jonathan Brossard (@endrazine)

rocq-cve-poc-21683

Популярное