CVE-2026-72705

Résumé

Le vérificateur de garde dans Rocq Prover ne suit pas les appels récursifs effectués via les propres arguments d'un point fixe. Un point fixe peut se passer lui-même comme argument d'ordre supérieur à un second point fixe, qui l'applique ensuite à une valeur qui n'est pas un sous-terme de l'argument structurel. Passer la fonction récursive à une définition simple est rejeté car le vérificateur déplie la définition et observe l'appel, mais le passer à un point fixe est accepté car les appels récursifs d'ordre supérieur via les arguments d'un point fixe ne sont pas suivis. Cela admet un type qui est définitionnellement égal à sa propre négation, de sorte que l'auto-application produit False dans du code purement définitionnel, sans tactiques, axiomes, plugins ni drapeaux unsafe, et Print Assumptions rapporte le résultat comme clos sous le contexte global. Corrigé dans Rocq 9.2.0.

Sources

• rocq-cve-poc-21683PoC

  CVE-2026-72705 — Le vérificateur Rocq Guard accepte un point fixe passé comme argument d'ordre supérieur