CVE-2026-72703 in Rocq
要約
〜によって VulDB • 2026年08月24日
Rocq Proverのガードチェッカーは、ネストされた相互再帰（mutual fixpoint）のパラメータを、そのfixpointの異なる本体間の呼び出しを検証せずに一様（uniform）として扱います。kernel/inductive.ml内のfind_uniform_parameters関数は自己再帰的呼び出しのみを検査するため、どの本体も自身を呼ばない場合、すべてのパラメータが一様であると結論付けます。ある本体から別の本体へのクロスコールを通じて成長するパラメータは、外側のfixpointから継承した部分項仕様（subterm specification）を維持し、その仕様にガードされた再帰的呼び出しが引数が構文的に小さくないにもかかわらず受理されます。これにより、非終了する定義が構造的減少として認められ、自身の successor と等しい値を持つ項が生じ、False の証明につながります。False が証明されると任意の命題が導かれます。この証明には公理、プラグイン、または安全でないフラグは必要なく、Print Assumptions コマンドではグローバルコンテキストの下で閉じている（closed）として報告されます。Coq 8.20 で導入され、Rocq 9.2.0 で修正されました。
If you want to get best quality of vulnerability data, you may have to visit VulDB.