一貫した公理から 0 = 1 をガードチェッカーの不動点再帰ツリー破損を経由して証明する。
| フィールド | 値 |
|---|---|
| バグ報告 | 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 (常に誤った制御フロー実装) |
| CVE | CVE-2026-72704 |
Rocq Prover のガードチェッカー(不動点の停止性チェッカー)は、帰納型の引数の
再帰ツリー表現がトランスポート(rew)によって変更された場合に、その再帰ツリーを
再検査しない。不動点は帰納型の型パラメータの再帰ツリーを暗黙のうちに破損させ得る。
そして最初の不動点を呼び出す2番目の不動点は、検証なしに破損した再帰ツリーを信頼し、
停止しない定義を構造的に減少するものとして受け入れてしまう。
このエクスプロイトは、CIC と一貫性のある2つの公理を使用する。これらは
一貫性公理(ユニバレンス公理)の直接の帰結である(0↔1 を入れ替える全単射は
Type 内にパス nat = nat を与え、それに沿ったトランスポートは 0 を 1 に送る)。
健全なガードチェッカーは、一貫性のある公理から False を導出してはならない。
このエクスプロイトの特徴:
Print Assumptions はそれら2つの公理のみを報告する — 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 のカーネルで検査された証明を信頼し、かつ univalence と整合する公理を使用しているあらゆるシステムが影響を受けます：
False を使用することができます。Rocq のガードチェッカーは、rectree を構築することによって fixpoint が構造的に減少していることを検証します。rectree とは、再帰呼び出しの各時点で再帰引数のどの部分項が利用可能かを追跡するツリーです。このバグは 2 段階の失敗です：
Rectree の破損: weird は Box A 上の fixpoint であり、wrap ケースで再帰引数に rew [Box] e（e : A = A に沿った transport）を適用します。ガードチェッカーは、transport が帰納型 Box を保持するためこれを受理しますが、パラメータ A の rectree は黙って変更されます — transport の後、ガードチェッカーの内部モデルは A を通じてどの値が流れるかを正確に追跡しなくなります。
未検査の信頼: loop は weird loop e (wrap _ (box _ n)) を呼び出します。ガードチェッカーは loop 自身の再帰呼び出しを検証しますが、ネストされた呼び出しについては weird の rectree を信頼します。weird の rectree が transport によって破損しているため、ガードチェッカーは 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 が得られる。
2つの公理:
e : nat = nat :> Type
e1 : rew [fun T => T] e in 0 = 1
は単一性公理の帰結である。単一性の下では、任意の全単射
f : nat → nat が Type 内に経路 nat = nat を与え、その経路に沿った
輸送は f として作用する。0↦1、1↦0、および n≥2 に対して
n↦n を送る全単射 swap01 はそのような全単射であり、swap01 0 = 1 が e1 を
証人立てする。
単一性は CIC と整合的であることが知られている（キュービカル型 理論モデルによって検証済み）。したがって、これらの公理が矛盾の 原因ではあり得ない — ガードチェッカーが原因である。
| 観点 | Rocq #22024（本バグ） | Rocq #22287 | Lean #14484 |
|---|---|---|---|
| バグ分類 | ガードチェッカーの rectree 破損 | 宇宙検査の状態デシンク | 推論キャッシュのポイズニング |
| 必要な公理 | 2（単一性と整合的） | なし | なし |
| エクスプロイトの複雑さ | 約30行 | 6行 | 約20行 |
| コンポーネント | ガードチェッカー（fixpoint） | モジュールシステム（ugraph フラグ） | 型チェッカー（opaque 宣言） |
| 修正状況 | PR #22027（オープン） | オープン | 修正済み（PR #14498） |