CVE-2026-72844 : Bug de solidité du noyau Lean 4

Prouver 0 = 1 sans axiomes via un contournement de la validation des projections inductives imbriquées.

Résumé de la vulnérabilité

Le noyau Lean 4 ne vérifie pas que la structure nommée dans une expression de projection correspond au type de la valeur projetée, et environment::add_inductive dans src/kernel/inductive.cpp ne vérifiait pas les types des applications inductives imbriquées qui sont remplacées par des types auxiliaires, de sorte que leurs arguments paramétriques échappaient à la vérification.

Un métaprogramme s'exécutant dans le processus Lean peut enregistrer une inductive imbriquée mal typée dont le constructeur applique une projection .proj C 0 à une valeur du type sans rapport W, et le noyau admet la déclaration par le chemin addDecl vérifié ordinaire avec une vérification maximale. Le résultat est une confusion de type produisant une preuve de False sans aucun axiome, à partir de laquelle n'importe quelle proposition — y compris 0 = 1 — peut être dérivée.

L'exploit :

• Utilise uniquement le chemin addDecl vérifié du noyau
• S'exécute avec --trust=0 (vérification maximale)
• Ne rapporte aucun axiome via #print axioms
• N'utilise ni sorry, ni unsafeCast, ni debug.skipKernelTC, ni FFI, ni altération de .olean

Utilisation

docker build -t lean-cve-poc .
docker run --rm lean-cve-poc

Sortie attendue sur une version vulnérable de Lean :

[*] Running ZeroEqOne.lean with --trust=0 ...
'bad' does not depend on any axioms
'boom' does not depend on any axioms
'zero_eq_one' does not depend on any axioms
zero_eq_one : 0 = 1

[!] VULNERABILITY CONFIRMED — CVE-2026-72844

    zero_eq_one : 0 = 1
    Depends on: no axioms

Sur une version corrigée de Lean, le noyau rejette l'inductive mal typée et le script indique que la version n'est pas vulnérable.

Impact

Tout système qui fait confiance aux preuves vérifiées par le noyau de Lean comme vérité de référence est concerné. Cela inclut :

• Logiciels formellement vérifiés : compilateurs, bibliothèques cryptographiques, contrats intelligents, avionique, automobile — toute démonstration de sûreté fondée sur une preuve Lean est invalide si elle est construite avec une version affectée.
• Code à preuve jointe (proof-carrying code) : une dépendance malveillante dans un paquet Lake peut silencieusement introduire des déclarations non fiables utilisées par le code en aval.
• Vérificateurs indépendants : il a été démontré que la même classe de bug contourne également le vérificateur de types indépendant Nanoda.

Détails techniques

La cause racine se situe dans la gestion par le noyau des types inductifs imbriqués. Lors de l'élimination d'une occurrence imbriquée I Ds is, le noyau doit vérifier que les arguments paramétriques Ds correspondent aux paramètres déclarés de l'inductive. Le code vulnérable ne vérifie pas que les expressions de projection (.proj) dans Ds référencent le nom de structure correct — un .proj C 0 w est accepté même lorsque w : W et W ≠ C.

Combiné à une collision de hachage (le noyau utilise les comparaisons Expr.hash dans sa vérification d'égalité définitionnelle), cela permet à un attaquant d'enregistrer des déclarations où l'affectation de type interne du noyau est en désaccord avec la sémantique réelle du terme, conduisant à une confusion de type et à une preuve de False.

Références

• NVD : CVE-2026-72844
• Avis VulnCheck
• Divulgation oss-security
• Problème Lean 4 #14576
• Correctif PR #14577
• Commit du correctif

Crédits

• Découverte du bug et PoC minimal : @kiranandcode
• Exploit CollatzLean original : @xrchz (Ramana Kumar)
• Correctif du noyau : Leonardo de Moura (PR #14577)
• Dépôt de la CVE et conditionnement du PoC : Jonathan Brossard (@endrazine)