endrazine/rocq-cve-poc-22287CVE-2026-72714 — рассинхронизация состояния проверки вселенной Rocq после закрытия модуля
Доказательство 0 = 1 без аксиом через десинхронизацию флага проверки вселенных в области модуля.
| Поле | Значение |
|---|---|
| Отчёт об ошибке | rocq-prover/rocq#22287 |
| Исправление | Нет (по состоянию на 2026-08-16 issue открыт) |
| Затронуто | Rocq ≤ 9.2.0 / Coq 8.x (все версии с Hurkens в stdlib) |
| CVSS 3.1 | AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N — 7.1 |
| CWE | CWE-488 (Exposure of Data Element to Wrong Session), CWE-20 (Improper Input Validation) |
| CVE | CVE-2026-72714 |
Модульная система Rocq Prover не обеспечивает должной области действия для флага
Local Unset Universe Checking. При использовании внутри модуля флаг
должен восстанавливаться в предыдущее состояние при закрытии модуля. Однако
граф вселенных (ugraph) хранит собственную копию флага, которая
выходит из синхронизации с глобальным состоянием при закрытии модуля.
После десинхронизации:
Test Universe Checking сообщает включено (глобальный флаг был восстановлен)ugraph проверка вселенных по-прежнему выключена (его копия не была восстановлена)При фактически отключённой проверке вселенных применяется парадокс
Хуркенса: TypeNeqSmallType.paradox использует тот факт, что Type@{u} и
Type@{v} при u < v могут быть перепутаны, когда ограничения вселенных
не применяются, что даёт прямое доказательство False.
Эксплойт:
Print Assumptions сообщает "Closed under the global context"Stdlib.Logic.Hurkens (часть стандартной библиотеки)docker build -t rocq-cve-poc-22287 .
docker run --rm rocq-cve-poc-22287
Ожидаемый вывод на уязвимой версии Rocq:
[*] Compiling ZeroEqOne.v ...
Universe Checking is on.
bad is defined
Closed under the global context
zero_eq_one is defined
Closed under the global context
[!] VULNERABILITY CONFIRMED
zero_eq_one : 0 = 1
Depends on: no axioms (closed under the global context)
Bug class: Universe checking state desync (CWE-488)
Root cause: ugraph retains stale Local Unset Universe Checking flag
Bug report: https://github.com/rocq-prover/rocq/issues/22287
Затронута любая система, которая доверяет проверенным ядром Rocq доказательствам:
.v в зависимости может
незаметно внести некорректные объявления, на которые опираются последующие доказательства.Граф универсумов (ugraph) в ядре содержит собственную копию
флага Universe Checking. Когда модуль использует Local Unset Universe Checking,
флаг изменяется как в глобальном состоянии, так и в ugraph. Когда
модуль закрывается, глобальное состояние восстанавливается из сохранённого состояния модуля,
но копия в ugraph не синхронизируется, из-за чего проверка универсумов
фактически остаётся отключённой.
┌─────────────────────────────────────────────────────┐
│ 1. Universes u v. Constraint u < v. │
│ → Declare universes with strict ordering │
├─────────────────────────────────────────────────────┤
│ 2. Module Off. │
│ Local Unset Universe Checking. │
│ End Off. │
│ → ugraph flag stays OFF after module closes │
├─────────────────────────────────────────────────────┤
│ 3. Test Universe Checking. → reports "on" (LIE) │
├─────────────────────────────────────────────────────┤
│ 4. eapply TypeNeqSmallType.paradox; reflexivity. │
│ → Kernel accepts universe-inconsistent proof │
│ → False proved with no axioms │
├─────────────────────────────────────────────────────┤
│ 5. zero_eq_one : 0 = 1 │
│ → Derived via exfalso │
└─────────────────────────────────────────────────────┘
| Аспект | Rocq #22287 (эта ошибка) | Lean #14484 | Lean #14576 |
|---|---|---|---|
| Пруф-ассистент | Rocq (Coq) | Lean 4 | Lean 4 |
| Класс ошибки | Рассинхронизация состояния в модульной системе | Отравление кэша вывода | Путаница типов через проекции |
| Сложность эксплойта | 6 строк | ~20 строк | ~50 строк |
| Система вселенных/типов | Проверка вселенных обойдена | Принимается непрозрачный FVar | Фантомные параметры выходят за пределы |
| Статус исправления | Открыта | Исправлено (PR #14498) | Исправлено (PR #14577) |