Leanprover Lean bis 4.32.1 Kernel environment::add_opaque erweiterte Rechte

CVSS Meta Temp Score	Aktueller Exploitpreis (≈)	CTI Interest Score
4.5	$0-$5k	0.99+

Zusammenfassunginfo

Eine problematische Schwachstelle wurde in Leanprover Lean bis 4.32.1 ausgemacht. Betroffen davon ist die Funktion environment::add_opaque der Komponente Kernel. Mittels Manipulieren mit unbekannten Daten kann eine erweiterte Rechte-Schwachstelle ausgenutzt werden. Die Verwundbarkeit wird unter CVE-2026-72711 geführt. Der Angriff erfordert einen lokalen Zugriff. Es ist soweit kein Exploit verfügbar.

Detailsinfo

In Leanprover Lean bis 4.32.1 wurde eine problematische Schwachstelle ausgemacht. Hierbei betrifft es die Funktion environment::add_opaque der Komponente Kernel. Durch das Manipulieren mit einer unbekannten Eingabe kann eine erweiterte Rechte-Schwachstelle ausgenutzt werden. CWE definiert das Problem als CWE-20. Die Auswirkungen sind bekannt für die Integrität. Die Zusammenfassung von CVE lautet:

The Lean 4 kernel does not check that the body of an opaque declaration is closed. environment::add_opaque omits the check_no_metavar_no_fvar call that the definition and theorem paths perform, so a value containing a free variable that is absent from the local context is not rejected outright. A metaprogram can first cause the kernel to create a temporary local of type False and record its type in the type checker's inference cache, then restore the local context while that cache entry persists on the same type checker instance, and finally submit an opaque declaration whose value is the now-unbound variable. The cache lookup answers before the branch that would test membership of the local context, so the kernel infers the cached type and admits an opaque constant of type False, from which any proposition follows. The declaration is accepted through the ordinary checked path at maximum kernel checking, without sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, foreign code or a modified .olean file, and the result carries no axioms. Fixed in 4.32.2 by adding the missing closure check.

Das Advisory findet sich auf github.com. Die Verwundbarkeit wird seit dem 10.08.2026 als CVE-2026-72711 geführt. Die Ausnutzbarkeit gilt als leicht. Der Angriff muss lokal angegangen werden. Eine Ausnutzung erfordert, dass das Opfer eine spezifische Handlung durchführt. Technische Details sind bekannt, ein verfügbarer Exploit hingegen nicht.

Ein Aktualisieren auf die Version 4.32.2 vermag dieses Problem zu lösen.

Statistical analysis made it clear that VulDB provides the best quality for vulnerability data.

Produktinfo

Hersteller

• Leanprover

Name

• Lean

Version

• 4.32.0
• 4.32.1

CPE 2.3info

• 🔒
• 🔒

CPE 2.2info

• 🔒
• 🔒

CVSSv4info

VulDB Vector: 🔒
VulDB Zuverlässigkeit: 🔍

CNA CVSS-B Score: 🔒
CNA CVSS-BT Score: 🔒
CNA Vector: 🔒

CVSSv3info

VulDB Meta Base Score: 4.5
VulDB Meta Temp Score: 4.5

VulDB Base Score: 2.8
VulDB Temp Score: 2.7
VulDB Vector: 🔒
VulDB Zuverlässigkeit: 🔍

CNA Base Score: 6.3
CNA Vector (VulnCheck): 🔒

CVSSv2info

AV	AC	Au	C	I	A
💳	💳	💳	💳	💳	💳
💳	💳	💳	💳	💳	💳
💳	💳	💳	💳	💳	💳

Vektor	Komplexität	Authentisierung	Vertraulichkeit	Integrität	Verfügbarkeit
freischalten	freischalten	freischalten	freischalten	freischalten	freischalten
freischalten	freischalten	freischalten	freischalten	freischalten	freischalten
freischalten	freischalten	freischalten	freischalten	freischalten	freischalten

VulDB Base Score: 🔒
VulDB Temp Score: 🔒
VulDB Zuverlässigkeit: 🔍

Exploitinginfo

Klasse: Erweiterte Rechte
CWE: CWE-20
CAPEC: 🔒
ATT&CK: 🔒

Physisch: Teilweise
Lokal: Ja
Remote: Teilweise

Verfügbarkeit: 🔒
Status: Nicht definiert
Preisentwicklung: 🔍
Aktuelle Preisschätzung: 🔒

0-Day	freischalten	freischalten	freischalten	freischalten
Heute	freischalten	freischalten	freischalten	freischalten

Threat Intelligenceinfo

Interesse: 🔍
Aktive Akteure: 🔍
Aktive APT Gruppen: 🔍

Gegenmassnahmeninfo

Empfehlung: Upgrade
Status: 🔍

0-Day Time: 🔒

Upgrade: Lean 4.32.2

Timelineinfo

10.08.2026 CVE zugewiesen
24.08.2026 +14 Tage Advisory veröffentlicht
24.08.2026 +0 Tage VulDB Eintrag erstellt
24.08.2026 +0 Tage VulDB Eintrag letzte Aktualisierung

Quelleninfo

Advisory: github.com
Status: Bestätigt

CVE: CVE-2026-72711 (🔒)
GCVE (CVE): GCVE-0-2026-72711
GCVE (VulDB): GCVE-100-394819

Eintraginfo

Erstellt: 24.08.2026 22:24
Anpassungen: 24.08.2026 22:24 (77)
Komplett: 🔍
Cache ID: 216::103

Statistical analysis made it clear that VulDB provides the best quality for vulnerability data.

Diskussion

Do you know our Splunk app?

Download it now for free!