CVE-2026-72704
中公開済み
Rocq Prover 9.2.0 までの Guard Checker は転送後に破損した再帰ツリーを信頼する
- 公開済み
- 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のガードチェッカーは、帰納型パラメータがtransportによって変更された後、そのパラメータの再帰的木表現を再チェックしません。fixpointは型間の等価性に沿った書き換えを再帰引数に適用でき、帰納型が保存されるためガードチェッカーはこれを受理しますが、パラメータに対して記録された再帰的木は変更されます。最初のfixpointを呼び出す2番目のfixpointは、検証なしに変更された再帰的木を継承するため、構造的に減少しない呼び出しが停止するものとして受理されます。その結果生じる非停止定義は、自然数が自身の後続と等しいこと、ひいてはFalseを証明し、そこから任意の命題が導かれます。この実証は、univalenceから導かれ、帰納構成の計算体系と整合する2つの公理を使用しているため、矛盾は仮定ではなくガードチェックに起因します。修正が提案されていますが、マージされていません。
ソース
CVE-2026-72704 — Rocq Guard Checkerがトランスポート後に破損した再帰ツリーを信頼する
責任ある使用
脆弱性情報は、自分が所有しているシステム、またはテストを許可されているシステムでのみ使用してください。 Kitploit は公開研究メタデータにリンクしており、エクスプロイト コードや悪意のあるペイロードは保存しません。