CVE-2026-72711

Résumé

Le noyau Lean 4 ne vérifie pas que le corps d'une déclaration opaque est clos. environment::add_opaque omet l'appel à check_no_metavar_no_fvar que les chemins de définition et de théorème effectuent, de sorte qu'une valeur contenant une variable libre absente du contexte local n'est pas rejetée d'emblée. Un métaprogramme peut d'abord amener le noyau à créer un local temporaire de type False et à enregistrer son type dans le cache d'inférence du vérificateur de types, puis restaurer le contexte local tandis que cette entrée de cache persiste sur la même instance de vérificateur de types, et enfin soumettre une déclaration opaque dont la valeur est la variable désormais non liée. La consultation du cache répond avant la branche qui testerait l'appartenance au contexte local, de sorte que le noyau infère le type mis en cache et admet une constante opaque de type False, à partir de laquelle toute proposition découle. La déclaration est acceptée via le chemin vérifié ordinaire à la vérification maximale du noyau, sans sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, code étranger ni fichier .olean modifié, et le résultat ne porte aucun axiome. Corrigé dans la version 4.32.2 par l'ajout de la vérification de clôture manquante.

Sources

• lean-cve-poc-14484PoC

  CVE-2026-72711 — Bug de solidité du noyau Lean 4 : empoisonnement du cache d'inférence