CVE-2026-72844

Résumé

Le noyau de 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 par typage les 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 exécuté 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 via le chemin ordinaire `addDecl` soumis à vérification, au niveau maximal de vérification du noyau, sans `sorry`, `unsafeCast`, `debug.skipKernelTC`, `addDeclWithoutChecking`, FFI, ni fichier `.olean` modifié. Il en résulte une confusion de type produisant une preuve de `False` ne portant aucun axiome, à partir de laquelle n'importe quelle proposition peut être dérivée. La preuve de concept publiée complète en outre deux expressions jusqu'à ce que leurs hachages et leurs profondeurs approximatives entrent en collision, ce qui neutralise la mise en cache du noyau ; c'est la technique utilisée pour atteindre la faille, et non sa cause. L'exploitation nécessite l'exécution d'un métaprogramme dans le processus, par exemple en construisant un projet ou en important une dépendance Lake malveillante.

• lean-cve-pocPoC

  CVE-2026-72844 : Exemple de preuve de « 0 = 1 » en exploitant une vulnérabilité dans le noyau de Lean 4.