CVE-2026-72714 — モジュールクローズ後に Rocq の宇宙（universe）チェック状態が非同期化される問題

モジュールスコープの宇宙チェックフラグの非同期化を利用し、公理なしで 0 = 1 を証明する。

フィールド	値
バグレポート	rocq-prover/rocq#22287
修正	なし（2026-08-16 時点でイシューはオープン）
影響範囲	Rocq ≤ 9.2.0 / Coq 8.x（stdlib に Hurkens を含むすべてのバージョン）
CVSS 3.1	`AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N` — 7.1
CWE	CWE-488（データ要素の誤ったセッションへの露出）、CWE-20（不適切な入力検証）
CVE	CVE-2026-72714

脆弱性の概要

Rocq Prover のモジュールシステムは、Local Unset Universe Checking フラグを適切にスコープ化できていません。モジュール内で使用された場合、このフラグはモジュールが閉じられた時点で以前の状態に復元されるべきです。しかし、宇宙グラフ（ugraph）はフラグの独自のコピーを保持しており、モジュールのクローズ時にグローバル状態と同期が取れなくなります。

非同期化が発生した後：

Test Universe Checking はオンを報告する（グローバルフラグは復元された）
ugraph は依然として宇宙チェックがオフのままである（そのコピーは復元されなかった）
そのためカーネルは、宇宙の整合性に反する項をエラーなしで受け入れてしまう

宇宙チェックが実質的に無効化されると、Hurkens のパラドックスが適用されます：TypeNeqSmallType.paradox は、宇宙制約が強制されない場合に u < v である Type@{u} と Type@{v} が混同され得るという事実を悪用し、False の直接的な証明を導き出します。

このエクスプロイトは：

公理、プラグイン、安全でない機能を一切使用しない
Print Assumptions は「Closed under the global context」と報告する
標準ライブラリの一部である Stdlib.Logic.Hurkens のみを必要とする
証明コードはわずか 6 行である

使用方法

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 のカーネル検証済み証明を信頼するあらゆるシステムが影響を受けます：

形式検証済みソフトウェア: CompCert（検証済み C コンパイラ）、CertiKOS （検証済み OS カーネル）、Iris（並行分離論理フレームワーク）、 MathComp — Rocq の証明に基づいて構築された安全性ケースは、証明環境でこのフラグの非同期が発生していた場合、無効となります。
証明付きコード: 依存関係にある悪意のある .v ファイルが、下流の証明が依存する不健全な宣言を黙って導入する可能性があります。
スマートコントラクト: 検証済みスマートコントラクト開発に Rocq を使用しているプロジェクト（例：ConCert）では、セキュリティ保証が無効化される可能性があります。

技術的詳細

根本原因

カーネル内の宇宙グラフ（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                             │
└─────────────────────────────────────────────────────┘

Lean 4 カーネルバグとの比較

観点	Rocq #22287（本バグ）	Lean #14484	Lean #14576
証明支援系	Rocq (Coq)	Lean 4	Lean 4
バグ分類	モジュールシステムにおける状態の非同期	推論キャッシュの汚染	射影による型の混同
エクスプロイトの複雑さ	6行	約20行	約50行
宇宙/型システム	宇宙チェックのバイパス	不透明なFVarが受理される	ファントムパラメータの脱出
修正状況	未解決	修正済み (PR #14498)	修正済み (PR #14577)

クレジット

バグ発見: Gaëtan Gilbert (@SkySkimmer)
PoC パッケージ化: Jonathan Brossard (@endrazine)

rocq-cve-poc-22287

人気