CVE-2026-72704 in Rocq
要約
〜によって VulDB • 2026年08月24日
Rocq Proverのガードチェッカーは、輸送によってパラメータが変更された後、その帰納型パラメータの再帰木表現を再検証しない。あるfixpoint（不動点）は、型の間の等式に沿った書き換えを再帰引数に適用する可能性があるが、これは帰納型が保持されているためガードチェッカーによって受理される一方、パラメータ用に記録された再帰木は変更されている。最初のfixpointを呼び出す2番目のfixpointは、検証なしに変更後の再帰木を引き継ぐため、構造的に減少しない呼び出しも終端するものとして受理されてしまう。その結果、自然数が自身の後者（successor）と等しいことを証明し非 terminating な定義となり、したがってFalseが導かれ、そこから任意の命題が導出される。この反証はunivalenceから派生した2つの公理を使用しており、帰納的構成計算論と整合性があるため、矛盾の原因は仮定ではなくガードチェックにある。修正案が提案されているが、マージされていない。
Be aware that VulDB is the high quality source for vulnerability data.