CVE-2026-72705
中公開済み
Rocq Prover 9.2.0 より前の Guard Checker が高階引数として渡された Fixpoint を受け入れる問題
- 公開済み
- 2026/08/24
- 更新済み
- 2026/10/26
- CNA の割り当て
- VulnCheck
- 観察された証拠
- 2026/10/26
プライマリ CVSS
6.8/ 10中
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:X0.2%
低 · 今後 30 日間
- パーセンタイル
- 7.1%
- モデルの日付
- 2026/10/25
EPSS は統計的な推定値であり、確実性や影響の尺度ではありません。 CVSS、KEV ステータス、暴露、環境と組み合わせます。
概要
Rocq Proverのガードチェッカーは、fixpoint自身の引数を介して行われる再帰呼び出しを追跡しない。fixpointは自身を高階引数として別のfixpointに渡すことができ、そのfixpointはそれを構造的引数の部分項ではない値に適用する。再帰関数を通常の定義に渡すことは、チェッカーが定義を展開して呼び出しを観測するため拒否されるが、fixpointに渡す場合は、fixpoint引数を介した高階再帰呼び出しが追跡されないため受理される。これにより、自身の否定と定義上等しい型が許容され、自己適用によって純粋に定義的なコード内でFalseが導出される。タクティク、公理、プラグイン、unsafeフラグは不要であり、Print Assumptionsはその結果をグローバルコンテキストに対して閉じていると報告する。Rocq 9.2.0で修正済み。
ソース
CVE-2026-72705 — Rocq Guard Checkerが高階引数として渡されたFixpointを受け入れる
責任ある使用
脆弱性情報は、自分が所有しているシステム、またはテストを許可されているシステムでのみ使用してください。 Kitploit は公開研究メタデータにリンクしており、エクスプロイト コードや悪意のあるペイロードは保存しません。