Rocq Prover jusqu'à 9.2.0 : état de vérification de l'univers désynchronisé après la fermeture d'un module
nvd · CVSS 4.0
CVSS:4.0/AV:L/AC:L/AT:N/PR:N/UI:P/VC:N/VI:H/VA:N/SC:N/SI:N/SA:N/E:X/CR:X/IR:X/AR:X/MAV:X/MAC:X/MAT:X/MPR:X/MUI:X/MVC:X/MVI:X/MVA:X/MSC:X/MSI:X/MSA:X/S:X/AU:X/R:X/V:X/RE:X/U:XFaible · 30 prochains jours
EPSS est une estimation statistique, et non une certitude ou une mesure d'impact. Combinez-le avec CVSS, le statut KEV, l'exposition et votre environnement.
Rocq Prover ne restaure pas la copie du drapeau de vérification des univers détenue par le graphe des univers lorsqu'un module ayant désactivé localement la vérification est fermé. Un `Unset Universe Checking` local à l'intérieur d'un module est censé ne durer que jusqu'à la fin du module, et le drapeau global est restauré, mais le graphe des univers conserve sa propre copie, qui reste désactivée. Les deux vues divergent alors : `Test Universe Checking` signale la vérification comme activée tandis que le noyau continue d'accepter des termes incohérents du point de vue des univers. La contrainte entre deux univers n'étant plus appliquée, le paradoxe de Hurkens s'applique et produit une preuve de `False`, dont découle n'importe quelle proposition. La preuve n'utilise aucun axiome, plugin ni fonctionnalité unsafe une fois le module fermé, et `Print Assumptions` la rapporte comme close sous le contexte global, de sorte que ni l'audit des hypothèses ni l'interrogation du drapeau ne reflètent l'état réel du noyau. Aucun correctif n'est disponible.
CVE-2026-72714 — État de vérification de l'univers Rocq désynchronisé après la fermeture d'un module
Utilisez les informations de vulnérabilité uniquement sur les systèmes que vous possédez ou que vous êtes autorisé à tester. Kitploit renvoie aux métadonnées de la recherche publique et ne stocke pas de code d'exploitation ni de charges utiles malveillantes.