CVE-2026-72703
Rocq Prover 8.20 から 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/25
EPSS は統計的な推定値であり、確実性や影響の尺度ではありません。 CVSS、KEV ステータス、暴露、環境と組み合わせます。
概要
Rocq Proverのガードチェッカーは、ネストされた相互フィックスポイントのパラメータを、そのフィックスポイントの異なる本体間の呼び出しを検査せずに均一であると扱います。kernel/inductive.mlのfind_uniform_parametersは自己再帰呼び出しのみを検査するため、どの本体も自身を呼び出さない場合、この関数はすべてのパラメータが均一であると結論付けます。したがって、ある本体から別の本体へのクロス呼び出しを通じて成長するパラメータは、外側のフィックスポイントから継承したsubterm specificationを保持したままになり、そのspecificationによってガードされた再帰呼び出しは、引数が構造的に小さくないにもかかわらず受け入れられます。非終了する定義が構造的に減少するものとして認められ、その結果、値が自身の後続と等しくなる項が得られ、ひいてはFalseの証明が得られ、そこから任意の命題が導かれます。この証明には公理、プラグイン、unsafeフラグは不要であり、Print Assumptionsはグローバルコンテキストの下で閉じていると報告します。Coq 8.20で導入され、Rocq 9.2.0で修正されました。
ソース
CVE-2026-72703 — Rocq Guard Checkerが未チェックの相互呼び出しにより非終了Fixpointを受け入れる
責任ある使用
脆弱性情報は、自分が所有しているシステム、またはテストを許可されているシステムでのみ使用してください。 Kitploit は公開研究メタデータにリンクしており、エクスプロイト コードや悪意のあるペイロードは保存しません。