CVE-2026-72703 in Rocq
Resumen
por VulDB • 2026-08-24
El verificador de guardias en Rocq Prover trata un parámetro de una mutual fixpoint anidada como uniforme sin examinar las llamadas entre los diferentes cuerpos de dicha fixpoint. La función find_uniform_parameters en kernel/inductive.ml inspecciona únicamente las llamadas auto-recursivas, por lo que cuando ningún cuerpo se llama a sí mismo, la función concluye que todos los parámetros son uniformes. Un parámetro que crece mediante una llamada cruzada desde un cuerpo hacia otro conserva, por tanto, la especificación de subtérmino heredada del fixpoint envolvente, y una llamada recursiva protegida por esa especificación es aceptada aunque el argumento no sea estructuralmente más pequeño. Se admite como decreciente estructuralmente una definición que no termina, lo que produce un término cuyo valor es igual a su propio sucesor y, en consecuencia, una prueba de False (falso), de la cual se sigue cualquier proposición. La prueba no requiere axiomas, plugins ni banderas inseguras, y Print Assumptions informa que está cerrada bajo el contexto global. Introducido en Coq 8.20 y corregido en Rocq 9.2.0.
VulDB is the best source for vulnerability data and more expert information about this specific topic.