CVE-2026-72704 — Проверяющий сторожевых условий Rocq доверяет повреждённому рекурсивному дереву после транспорта

Доказательство 0 = 1 из согласованных аксиом через повреждение fixpoint rectree в проверяющем сторожевых условий.

Поле	Значение
Отчёт об ошибке	rocq-prover/rocq#22024
Исправление	PR #22027 (открыт)
Затронуто	Rocq ≤ 9.2.0 / Coq 8.x (все версии с проверяющим сторожевых условий)
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-72704

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

Проверяющий сторожевых условий Rocq Prover (проверяющий завершаемость для fixpoint) не выполняет повторную проверку представления rectree аргументов индуктивного типа, когда они изменяются посредством транспорта (rew). Fixpoint может незаметно повредить rectree для параметра типа индуктивного типа, а второй fixpoint, вызывающий первый, доверяет повреждённому rectree без проверки, принимая незавершающееся определение как структурно убывающее.

Эксплойт использует две аксиомы, которые согласованы с CIC — они являются прямыми следствиями аксиомы унивалентности (биекция, меняющая местами 0↔1, даёт путь nat = nat в Type, вдоль которого транспорт переводит 0 в 1). Корректный проверяющий сторожевых условий не должен выводить False из согласованных аксиом.

Эксплойт:

Использует только две согласованные аксиомы (следствия унивалентности)
Print Assumptions сообщает только об этих двух аксиомах — никаких False, никаких sorry
Никаких плагинов, небезопасных функций или манипуляций с вселенными
Проверяющий сторожевых условий — единственный источник некорректности

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

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

Ожидаемый вывод на уязвимой версии Rocq:

[*] Compiling ZeroEqOne.v with rocq compile ...

zero_eq_one is defined
Axioms:
e : nat = nat
e1 : rew [fun T : Type => T] e in 0 = 1

[!] VULNERABILITY CONFIRMED

    zero_eq_one : 0 = 1
    Axioms used: e (nat = nat), e1 (transport sends 0 to 1)
    These axioms are consistent (consequences of univalence).
    A sound guard checker must not derive False from them.

    Bug class:  Guard checker rectree corruption (CWE-670)
    Root cause: fixpoints can alter rectrees via transport; nested
                fixpoints trust the corrupted rectree without recheck
    Bug report: https://github.com/rocq-prover/rocq/issues/22024

Влияние

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

Разработки HoTT: любой проект на Rocq, использующий аксиому унивалентности (или пропозициональную экстенсиональность, которая может вызвать тот же класс ошибок), может иметь свои проверенные на структурную рекурсию неподвижные точки молча принятыми, несмотря на незавершаемость.
Формально верифицированное программное обеспечение: CompCert, CertiKOS, Iris и любой проект, добавляющий пользовательские аксиомы, согласующиеся с CIC, подвергается риску, если проверка структурной рекурсии является единственной гарантией завершаемости.
Код с доказательствами (proof-carrying code): вредоносная зависимость может внедрить две аксиомы и повреждённую неподвижную точку, а затем использовать False в дальнейшем.

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

Ошибка проверки структурной рекурсии

Проверка структурной рекурсии в Rocq удостоверяется, что неподвижные точки структурно убывают, путём построения rectree — дерева, которое отслеживает, какие подтермы рекурсивного аргумента доступны при каждом рекурсивном вызове. Ошибка представляет собой двухэтапный сбой:

Повреждение rectree: weird — это неподвижная точка на Box A, которая применяет rew [Box] e (транспорт вдоль e : A = A) к рекурсивному аргументу в случае wrap. Проверка структурной рекурсии принимает это, поскольку транспорт сохраняет индуктивный тип Box, но rectree для параметра A молча изменяется — после транспорта внутренняя модель проверки структурной рекурсии больше не отслеживает точно, какие значения проходят через A.
Непроверенное доверие: loop вызывает weird loop e (wrap _ (box _ n)). Проверка структурной рекурсии проверяет собственные рекурсивные вызовы loop, но доверяет rectree weird для вложенного вызова. Поскольку rectree weird был повреждён транспортом, проверка структурной рекурсии ошибочно заключает, что loop структурно убывает.

Противоречие

Обманув проверку структурной рекурсии, loop принимается, несмотря на незавершаемость. Доказательство затем показывает:

loop 1 = S (loop 1)

путём развёртывания loop и weird и использования e1, чтобы показать, что transport отправляет box nat 0 в box nat 1, который возвращается обратно в loop. Поскольку ∀ n, n ≠ S n доказуемо по индукции, loop 1 = S (loop 1) даёт False, а из него 0 = 1.

Почему аксиомы непротиворечивы

Две аксиомы:

e  : nat = nat :> Type
e1 : rew [fun T => T] e in 0 = 1

являются следствиями аксиомы унивалентности. При унивалентности любая биекция f : nat → nat даёт путь nat = nat в Type, и перенос вдоль этого пути действует как f. Биекция swap01, которая переводит 0↦1, 1↦0 и n↦n для n≥2, является такой биекцией, причём swap01 0 = 1 свидетельствует о e1.

Известно, что унивалентность согласуется с CIC (подтверждено моделями кубической теории типов). Следовательно, эти аксиомы не могут быть источником противоречия — им является проверщик guard.

Сравнение с другими PoC

Аспект	Rocq #22024 (эта ошибка)	Rocq #22287	Lean #14484
Класс ошибки	Повреждение rectree в проверщике guard	Рассинхронизация состояния проверки вселенных	Отравление кэша вывода
Требуемые аксиомы	2 (согласуются с унивалентностью)	Нет	Нет
Сложность эксплойта	~30 строк	6 строк	~20 строк
Компонент	Проверщик guard (fixpoint)	Система модулей (флаг ugraph)	Проверщик типов (opaque decl)
Статус исправления	PR #22027 (открыт)	Открыт	Исправлено (PR #14498)

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

Обнаружение ошибки: Yann Leray (@yannl35133)
Подготовка PoC: Jonathan Brossard (@endrazine)

rocq-cve-poc-22024

Популярное