CVE-2026-72705
Vulnérabilité moyenne dans rocq (rocq-prover)
Description
The guard checker in Rocq Prover does not follow recursive calls made through a fixpoint's own arguments. A fixpoint may pass itself as a higher-order argument to a second fixpoint, which then applies it to a value that is not a subterm of the structural argument. Passing the recursive function to a plain definition is rejected because the checker unfolds the definition and observes the call, but passing it to a fixpoint is accepted because higher-order recursive calls through fixpoint arguments are not tracked. This admits a type that is definitionally equal to its own negation, so self-application produces False in purely definitional code, without tactics, axioms, plugins or unsafe flags, and Print Assumptions reports the result as closed under the global context. Fixed in Rocq 9.2.0.
Gravité et risque d'exploitation
CVE-2026-72705 obtient un score CVSS de 6.8/10, soit une gravité moyenne. Selon le modèle EPSS, la probabilité qu'elle soit exploitée dans les 30 prochains jours est de 0.18 %, ce qui la place devant 6.7 % des CVE référencées.
Que faire ?
- Vérifiez si rocq (versions 0, <9.2.0) est présent sur votre parc.
- Appliquez le correctif ou la version corrigée indiqués dans les références de l'éditeur.
- À défaut de correctif, limitez l'exposition (filtrage réseau, désactivation du composant).
- Automatisez la détection : les agents CVE Heimdall (gratuits, open source) corrèlent l'inventaire de vos serveurs avec la base CVE.