ガードチェッカーの fixpoint バイパスを通じてラッセルのパラドックスを利用し、0 = 1 を公理なしで証明する。
Claude Opus 4.6 (Anthropic) により自律的に発見。
| フィールド | 値 |
|---|---|
| バグレポート | rocq-prover/rocq#21683 |
| 修正 | PR #21684 |
| 影響範囲 | Rocq ≤ 9.1.0 / ガードチェッカーを備えるすべての Coq バージョン |
| 修正済み | 9.2.0 |
| 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-72705 |
ガードチェッカーは、自身を別の fixpoint への高階引数として渡し、その fixpoint が構造引数の非部分項に対して自身を呼び出すような fixpoint を受け入れます。再帰関数を Definition（fixpoint ではない定数）に渡すことは正しく拒否されます — ガードチェッカーはそれを展開し、問題のある呼び出しを検出します。しかし、Fixpoint に渡す場合は誤って受け入れられます。
これにより、4 行でラッセル流のパラドックスが生じます:
Definition delta (x : russell 1) : False := x x.
Definition omega : False := delta delta.
ここで russell 1 は定義上 russell 1 -> False と等しく、これは自身の否定となる型である。自己適用により直接 False が得られる。
このエクスプロイトは：
Print Assumptions は 「Closed under the global context」 と報告するFalse の証明全体は 4 行の関数型コードであるQed なし — 純粋に定義によるものdocker build -t rocq-cve-poc-21683 .
docker run --rm rocq-cve-poc-21683
Rocqのカーネル検証済み証明を信頼するあらゆるシステムが影響を受けます：
iterate_to_neg f n seed :=
match n with
| 0 => f seed -> False (* negate after n steps *)
| S m => iterate_to_neg f m seed
end
russell n :=
match n with
| 0 => True
| S m => iterate_to_neg russell 1 (S m) (* passes ITSELF *)
end
ガードチェッカーは russell を拒否すべきです。なぜなら、russell は自身を高階引数として iterate_to_neg に渡し、iterate_to_neg がそれを S m（n の部分項ではない）に対して呼び出すからです。しかし、チェッカーは直接的な再帰呼び出しのみを追跡しており、高階不動点引数を介した呼び出しは追跡していません。
russell 1 = iterate_to_neg russell 1 1
= iterate_to_neg russell 0 1
= russell 1 -> False
したがって russell 1 ≡ russell 1 -> False となる。これは古典的なラッセル集合、すなわち自分自身を含まないすべての集合の集合である。自己適用を行うと次のようになる：
delta : russell 1 -> False (* russell 1 = russell 1 -> False *)
delta x := x x (* x : russell 1 = russell 1 -> False *)
omega : False
omega := delta delta (* delta : russell 1 -> False = russell 1 *)
このバグは、Tristan Stérin (@tcosmo) がセットアップした夜間のファジング実行中に、Claude Opus 4.6 によって自律的に発見されたもので、ガードチェッカーに関する Yannick Forster (@yforster) からのヒントに基づいています。AI は高階不動点バイパスパターンを特定し、最小限の iterate_to_neg/russell エクスプロイトを構築しました。
参照: Zulip thread