CVE-2026-72703

Resumen

El verificador de guardas en Rocq Prover trata un parámetro de un punto fijo mutuo anidado como uniforme sin examinar las llamadas entre los diferentes cuerpos de ese punto fijo. find_uniform_parameters en kernel/inductive.ml inspecciona solo las llamadas autorrecursivas, por lo que cuando ningún cuerpo se llama a sí mismo, la función concluye que cada parámetro es uniforme. Un parámetro que crece a través de una llamada cruzada de un cuerpo a otro, por lo tanto, mantiene la especificación de subtérmino que heredó del punto fijo envolvente, y una llamada recursiva protegida por esa especificación es aceptada aunque el argumento no sea estructuralmente menor. Una definición no terminante es admitida como estructuralmente decreciente, lo que produce un término cuyo valor es igual a su propio sucesor y, por lo tanto, una prueba de Falso, de la cual se deduce cualquier proposición. La prueba no requiere axiomas, plugins o banderas inseguras y Print Assumptions lo reporta como cerrado bajo el contexto global. Introducido en Coq 8.20 y corregido en Rocq 9.2.0.

Fuentes

• rocq-cve-poc-21682PoC

  CVE-2026-72703 — El verificador Rocq Guard acepta un punto fijo no terminante mediante llamadas cruzadas no verificadas