モジュールファンクタのインライン化による証明監査のバイパス — 2020年以降未修正。
Print Assumptions は、ある定義がモジュール型の Parameter Inline を通じて呼び出し元に到達した場合に、その定義が宇宙チェックを無効にして構築されたことを報告できない。ファンクタの適用はパラメータの本体をインライン化し、Unset Universe Checking コンテキストの記録を破棄するため、結果として得られる定数には安全でない操作の痕跡が一切残らない。
したがって、あるモジュールは宇宙の矛盾を利用して False を証明でき、Print Assumptions は依存する証明をグローバルコンテキストの下で閉じているものとして報告する — 公理も、安全でないフラグも見えない。
coqchk は生成されたコンパイル済み .vo ファイルを確かに拒否するが、プロセス内の仮定監査（Print Assumptions）はこの問題を検出しない。
docker build -t rocq-cve-poc-12155 .
docker run --rm rocq-cve-poc-12155
脆弱なバージョン（Rocq 8.11 – 9.2.0、およびモジュールシステムを備えたすべての Coq 8.x）では、出力は 0 = 1 の証明を確認し、Print Assumptions はそれを閉じているものとして報告する。
Print Assumptions を唯一の完全性チェックとして依存しているあらゆるワークフローが影響を受ける可能性がある：
.v ファイルが、仮定監査を通過する不健全な宣言を導入する可能性があるcoqchk を日常的に実行していないあらゆるプロジェクトモジュール型が Parameter Inline を宣言すると、ファンクタの適用はパラメータの本体を呼び出し元コンテキストにインライン化する。このインライン化は、元の定義が Unset Universe Checking の下で生成されたことを記録したメタデータを破棄する。そのため、宇宙グラフはインライン化された本体からの矛盾した宇宙制約を受け入れ、Print Assumptions は安全でないコンテキストの痕跡を一切見ることができない。
このバグは2020年から未解決であり（Coq issue #12155）、プロジェクトの dev/doc/critical-bugs.md に文書化されている。Rocq 9.2.0 の時点で修正はマージされていない。
| 項目 | 値 |
|---|---|
| CVE | CVE-2020-37268 |
| 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-778 — 不十分なログ記録 |
| 製品 | 影響を受けるバージョン | 修正済み |
|---|---|---|
| Coq | 8.11 – 8.20 | 未修正 |
| Rocq Prover | 8.20 – 9.2.0 | 未修正 |
.vo ファイルに対して coqchk を実行する。coqchk は Print Assumptions が見逃す宇宙の矛盾を検出する。Unset Universe Checking の下でコンパイルされた Parameter Inline を持つモジュール型が必要である。| バグ報告 | rocq-prover/rocq#12155 |
| 重大バグ文書 | dev/doc/critical-bugs.md |
| VulnCheck アドバイザリ | vulncheck.com |
| 日付 | イベント |
|---|---|
| 2020 | Jason Gross によりバグが報告される（coq/coq#12155） |
| 2020–2026 | バグは未解決のまま、critical-bugs.md に文書化される |
| 2026-08-24 | CVE-2020-37268 が VulnCheck により公開される |
| 2026-08-24 | Docker で再現可能な PoC が公開される |