CVE-2026-72714
Rocq Prover 9.2.0 までにおけるモジュールクローズ後のユニバースチェック状態の非同期化
- 公開済み
- 2026/08/24
- 更新済み
- 2026/10/26
- CNA の割り当て
- VulnCheck
- 観察された証拠
- 2026/10/26
プライマリ CVSS
nvd · CVSS 4.0
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/E:X/CR:X/IR:X/AR:X/MAV:X/MAC:X/MAT:X/MPR:X/MUI:X/MVC:X/MVI:X/MVA:X/MSC:X/MSI:X/MSA:X/S:X/AU:X/R:X/V:X/RE:X/U:X低 · 今後 30 日間
- パーセンタイル
- 7.1%
- モデルの日付
- 2026/10/27
EPSS は統計的な推定値であり、確実性や影響の尺度ではありません。 CVSS、KEV ステータス、暴露、環境と組み合わせます。
概要
Rocq Proverは、ローカルでチェックを無効化したモジュールが閉じられた際に、universe graph側のuniverse checkingフラグのコピーを復元しない。モジュール内でのローカルな`Unset Universe Checking`はモジュール終了までのみ有効であることが期待され、グローバルフラグは復元されるが、universe graphは独自のコピーを保持しており、それが無効のまま残される。その結果、2つのビューが矛盾する。`Test Universe Checking`はチェックを有効として報告する一方で、カーネルはuniverse不整合な項を受け入れ続ける。2つのuniverse間の制約がもはや強制されないため、Hurkensのパラドックスが適用可能となり、`False`の証明が導かれ、そこから任意の命題が導かれる。この証明はモジュールが閉じられた後は公理、プラグイン、unsafe機能を一切使用せず、`Print Assumptions`はこれをグローバルコンテキストの下で閉じていると報告するため、仮定の監査もフラグの問い合わせも実際のカーネル状態を反映しない。修正は利用可能ではない。
ソース
CVE-2026-72714 — モジュールクローズ後に Rocq の Universe チェック状態が同期ずれを起こす
責任ある使用
脆弱性情報は、自分が所有しているシステム、またはテストを許可されているシステムでのみ使用してください。 Kitploit は公開研究メタデータにリンクしており、エクスプロイト コードや悪意のあるペイロードは保存しません。