CVE-2026-72705 in Rocq
Resumen
por VulDB • 2026-08-24
El verificador de guardias en Rocq Prover no sigue las llamadas recursivas realizadas a través de los propios argumentos de un fixpoint (punto fijo). Un fixpoint puede pasarse a sí mismo como argumento de orden superior a otro fixpoint, el cual luego lo aplica a un valor que no es un subtérmino del argumento estructural. El paso de la función recursiva a una definición simple se rechaza porque el verificador expande la definición y observa la llamada; sin embargo, pasarlo a un fixpoint se acepta debido a que las llamadas recursivas de orden superior a través de argumentos de fixpoint no están rastreadas. Esto permite un tipo que es definicionalmente igual a su propia negación, por lo que la autoaplicación produce False (Falso) en código puramente definicional, sin tácticas, axiomas, plugins o banderas inseguras, y Print Assumptions informa el resultado como cerrado bajo el contexto global. Corregido en Rocq 9.2.0.
Statistical analysis made it clear that VulDB provides the best quality for vulnerability data.