CVE-2026-72705

Resumen

El verificador de guardas en Rocq Prover no sigue las llamadas recursivas realizadas a través de los propios argumentos de un punto fijo. Un punto fijo puede pasarse a sí mismo como un argumento de orden superior a un segundo punto fijo, el cual luego lo aplica a un valor que no es un subtérmino del argumento estructural. Pasar la función recursiva a una definición simple es rechazado porque el verificador despliega la definición y observa la llamada, pero pasarlo a un punto fijo es aceptado porque las llamadas recursivas de orden superior a través de argumentos de punto fijo no son rastreadas. Esto admite un tipo que es definicionalmente igual a su propia negación, por lo que la autoaplicación produce Falso en código puramente definicional, sin tácticas, axiomas, plugins o flags inseguros, y Print Assumptions informa el resultado como cerrado bajo el contexto global. Corregido en Rocq 9.2.0.

Fuentes

• rocq-cve-poc-21683PoC

  CVE-2026-72705 — El verificador Rocq Guard acepta un Fixpoint pasado como argumento de orden superior