CVE-2026-72711
Lean 4 vor 4.32.2 Kernel akzeptiert opake Deklaration mit einer ungebundenen freien Variable
- Veröffentlicht
- 24.08.2026
- Aktualisiert
- 26.10.2026
- CNA zuweisen
- VulnCheck
- Beweise beobachtet
- 26.10.2026
Primäres CVSS
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:XNiedrig · nächste 30 Tage
- Perzentil
- 7,1 %
- Modelldatum
- 25.10.2026
EPSS ist eine statistische Schätzung, keine Gewissheit oder ein Maß für die Auswirkung. Kombinieren Sie es mit CVSS, KEV-Status, Belichtung und Ihrer Umgebung.
Zusammenfassung
Der Lean-4-Kernel prüft nicht, ob der Rumpf einer opaken Deklaration abgeschlossen ist. environment::add_opaque lässt den Aufruf check_no_metavar_no_fvar weg, den die Pfade für Definitionen und Theoreme durchführen, sodass ein Wert, der eine freie Variable enthält, die im lokalen Kontext fehlt, nicht sofort abgelehnt wird. Ein Metaprogramm kann zunächst bewirken, dass der Kernel ein temporäres Lokal vom Typ False erzeugt und dessen Typ im Inferenz-Cache des Type Checkers einträgt, dann den lokalen Kontext wiederherstellen, während dieser Cache-Eintrag auf derselben Type-Checker-Instanz bestehen bleibt, und schließlich eine opake Deklaration einreichen, deren Wert die nun ungebundene Variable ist. Die Cache-Abfrage antwortet vor dem Zweig, der die Zugehörigkeit zum lokalen Kontext prüfen würde, sodass der Kernel den zwischengespeicherten Typ ableitet und eine opake Konstante vom Typ False zulässt, aus der jede Aussage folgt. Die Deklaration wird über den gewöhnlichen geprüften Pfad bei maximaler Kernel-Prüfung akzeptiert, ohne sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, Fremdcode oder eine modifizierte .olean-Datei, und das Ergebnis trägt keine Axiome. Behoben in 4.32.2 durch Hinzufügen der fehlenden Abschlussprüfung.
Quellen
CVE-2026-72711 — Lean-4-Kernel-Korrektheitsfehler: Vergiftung des Inferenz-Caches
Verantwortungsvoller Umgang
Verwenden Sie Schwachstelleninformationen nur auf Systemen, die Sie besitzen oder zu deren Testen Sie berechtigt sind. Kitploit verlinkt auf öffentliche Forschungsmetadaten und speichert keinen Exploit-Code oder bösartige Payloads.