ガードチェッカーの均一パラメータバイパスにより、公理なしで 0 = 1 を証明する。
Rocq カーネルのガードチェッカー（fixpoint 停止性検証器）は、ネストされた相互 fixpoint のすべてのパラメータを、fixpoint の本体間の呼び出しを検査することなく均一（uniform）とみなします。kernel/inductive.ml 内の関数 find_uniform_parameters は自己再帰呼び出しのみを検査します。本体が自身を呼び出さない場合、すべてのパラメータが均一と判定されます。相互呼び出しを通じて増大するパラメータは、誤った subterm 指定を保持したままとなり、引数が構造的に小さくないにもかかわらず再帰呼び出しが受け入れられます。
これにより、False を証明する非停止の定義が許容され、そこから任意の命題が導かれます — 0 = 1 を含みます。
この証明には公理、タクティク、プラグイン、危険なフラグは一切不要です。Print Assumptions はこれをグローバルコンテキストの下で閉じていると報告します。
docker build -t rocq-cve-poc-21682 .
docker run --rm rocq-cve-poc-21682
脆弱なバージョン（Rocq 8.20 – <9.2.0）では、出力は公理なしで 0 = 1 の証明が成立することを確認します。
修正済みのバージョン（Rocq ≥9.2.0）では、ガードチェッカーがこの fixpoint を拒否します。
Rocq/Coq のカーネル検証済み証明に依存するシステムは、追加の緩和策なしに脆弱なバージョンで実行している場合、影響を受ける可能性があります：
.v ファイルが不健全な宣言を導入しうる場合kernel/inductive.ml 内の find_uniform_parameters は、相互 fixpoint の各本体における自己再帰呼び出しのみを検査します。どの本体にも自己再帰呼び出しが含まれない場合（すべての呼び出しが本体間の相互呼び出しである場合）、すべてのパラメータが均一としてマークされます。相互呼び出しを通じて実際に変化するパラメータは誤った subterm 指定を保持したままとなり、ガードチェッカーが構造的に減少しない引数に対する再帰呼び出しを受け入れることを許してしまいます。
| 項目 | 値 |
|---|---|
| CVE | CVE-2026-72703 |
| CVSS 3.1 | AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N — 7.1 (High) |
| CVSS 4.0 | AV:L/AC:L/AT:N/PR:N/UI:P/VC:N/VI:H/VA:N/SC:N/SI:N/SA:N — 6.8 (Medium) |
| CWE | CWE-670 — 常に不正確な制御フローの実装 |
| 製品 | 影響あり | 修正済み |
|---|---|---|
| Rocq Prover | 8.20 – <9.2.0 | 9.2.0 |
.vo ファイルに対して coqchk を実行してください。| バグ報告 | rocq-prover/rocq#21682 |
| 修正 | rocq-prover/rocq#21684 |
| VulnCheck アドバイザリ | vulncheck.com |
| 日付 | イベント |
|---|---|
| 2025 | バグ報告（rocq-prover/rocq#21682） |
| 2025 | 修正が Rocq 9.2.0 にマージ（PR #21684） |
| 2026-08-24 | CVE-2026-72703 が VulnCheck により公開 |
| 2026-08-24 | Docker で再現可能な PoC を公開 |