CVE-2026-72703 — Проверяющий guard checker Rocq принимает незавершающуюся фиксированную точку через непроверенные перекрёстные вызовы

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

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

Guard checker ядра Rocq (верификатор завершаемости фиксированных точек) считает все параметры вложенной взаимной фиксированной точки равномерными, не исследуя вызовы между телами фиксированной точки. Функция find_uniform_parameters в kernel/inductive.ml проверяет только самовызовы; если ни одно тело не вызывает само себя, каждый параметр признаётся равномерным. Параметр, который растёт через перекрёстный вызов, может затем сохранить некорректную спецификацию подтерма, и рекурсивный вызов принимается, даже если его аргумент не является структурно меньшим.

Это допускает незавершающееся определение, доказывающее False, из которого следует любое утверждение — включая 0 = 1.

Доказательство не требует аксиом, тактик, плагинов или небезопасных флагов. Print Assumptions сообщает, что оно замкнуто относительно глобального контекста.

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

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

На уязвимой версии (Rocq 8.20 – <9.2.0) вывод подтверждает доказательство 0 = 1 без аксиом.

На исправленной версии (Rocq ≥9.2.0) guard checker отвергает фиксированную точку.

Влияние

Любая система, полагающаяся на доказательства, проверенные ядром Rocq/Coq, может быть затронута, если она работает на уязвимой версии без дополнительных мер защиты:

• Формально верифицированные компиляторы (CompCert)
• Верифицированные ядра ОС (CertiKOS)
• Фреймворки separation logic (Iris)
• Математические библиотеки (MathComp)
• Proof-carrying code, где вредоносный файл .v в зависимости может внести некорректные объявления
• Верифицированные смарт-контракты (ConCert)

Первопричина

find_uniform_parameters в kernel/inductive.ml проверяет только самовызовы внутри каждого тела взаимной фиксированной точки. Когда ни одно тело не содержит самовызова (все вызовы — перекрёстные между телами), каждый параметр помечается как равномерный. Параметр, который фактически изменяется при перекрёстных вызовах, сохраняет некорректную спецификацию подтерма, что позволяет guard checker принять рекурсивный вызов с аргументом, не являющимся структурно меньшим.

Оценка

Поле	Значение
CVE	CVE-2026-72703
CVSS 3.1	AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N — 7.1 (High)
CVSS 4.0	AV:L/AC:L/AT:N/PR:N/UI:P/VC:N/VI:H/VA:N/SC:N/SI:N/SA:N — 6.8 (Medium)
CWE	CWE-670 — Always-Incorrect Control Flow Implementation

Затронутые версии

Продукт	Затронуты	Исправлено
Rocq Prover	8.20 – <9.2.0	9.2.0

Меры защиты

• Обновитесь до Rocq 9.2.0 или более поздней версии.
• Запускайте coqchk для скомпилированных файлов .vo в качестве дополнительной меры защиты.

Ссылки

Отчёт об ошибке	rocq-prover/rocq#21682
Исправление	rocq-prover/rocq#21684
Рекомендация VulnCheck	vulncheck.com

Хронология

Дата	Событие
2025	Об ошибке сообщено (rocq-prover/rocq#21682)
2025	Исправление объединено (PR #21684) в Rocq 9.2.0
2026-08-24	CVE-2026-72703 опубликован VulnCheck
2026-08-24	Опубликован воспроизводимый в Docker PoC

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

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