Leanprover Lean 4 bis 4.32.1/4.33.0-rc1 Kernel Type Checking src/kernel/inductive.cpp add_inductive erweiterte Rechte

CVSS Meta Temp ScoreAktueller Exploitpreis (≈)CTI Interest Score
5.0$0-$5k0.00

Zusammenfassunginfo

Eine als problematisch eingestufte Schwachstelle wurde in Leanprover Lean 4 bis 4.32.1/4.33.0-rc1 festgestellt. Es geht dabei um die Funktion environment::add_inductive der Datei src/kernel/inductive.cpp der Komponente Kernel Type Checking. Mittels Manipulieren mit unbekannten Daten kann eine erweiterte Rechte-Schwachstelle ausgenutzt werden. Diese Verwundbarkeit ist als CVE-2026-72844 gelistet. Die Umsetzung des Angriffs hat dabei lokal zu erfolgen. Es existiert kein Exploit.

Detailsinfo

Eine Schwachstelle wurde in Leanprover Lean 4 bis 4.32.1/4.33.0-rc1 entdeckt. Sie wurde als problematisch eingestuft. Dies betrifft die Funktion environment::add_inductive der Datei src/kernel/inductive.cpp der Komponente Kernel Type Checking. Durch Manipulieren mit einer unbekannten Eingabe kann eine erweiterte Rechte-Schwachstelle ausgenutzt werden. Klassifiziert wurde die Schwachstelle durch CWE als CWE-843. Auswirkungen hat dies auf Vertraulichkeit, Integrität und Verfügbarkeit. Die Zusammenfassung von CVE lautet:

The Lean 4 kernel does not verify that the structure named in a projection expression matches the type of the value being projected, and environment::add_inductive in src/kernel/inductive.cpp did not type check the nested inductive applications that are replaced by auxiliary types, so their parametric arguments escaped checking. A metaprogram running in the Lean process can register an ill-typed nested inductive whose constructor applies a .proj C 0 projection to a value of the unrelated type W, and the kernel admits the declaration through the ordinary checked addDecl path at maximum kernel checking, without sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, FFI, or a modified .olean file. The result is a type confusion yielding a proof of False that carries no axioms, from which any proposition can be derived. The published proof of concept additionally pads two expressions until their hashes and approximate depths collide, which defeats kernel caching; that is the technique used to reach the flaw, not its cause. Exploitation requires running a metaprogram in-process, for example by building a project or importing a malicious Lake dependency.

Bereitgestellt wird das Advisory unter github.com. Die Verwundbarkeit wird seit dem 10.08.2026 mit der eindeutigen Identifikation CVE-2026-72844 gehandelt. Die Ausnutzbarkeit gilt als leicht. Umgesetzt werden muss der Angriff lokal. Um eine Ausnutzung durchzusetzen, muss eine erweiterte Authentisierung umgesetzt werden. Eine Ausnutzung erfordert, dass das Opfer eine spezifische Handlung durchführt. Zur Schwachstelle sind technische Details bekannt, ein verfügbarer Exploit jedoch nicht.

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

If you want to get the best quality for vulnerability data then you always have to consider VulDB.

Produktinfo

Hersteller

Name

Version

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: 5.1
VulDB Meta Temp Score: 5.0

VulDB Base Score: 4.0
VulDB Temp Score: 3.8
VulDB Vector: 🔒
VulDB Zuverlässigkeit: 🔍

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

CVSSv2info

AVACAuCIA
💳💳💳💳💳💳
💳💳💳💳💳💳
💳💳💳💳💳💳
VektorKomplexitätAuthentisierungVertraulichkeitIntegritätVerfügbarkeit
freischaltenfreischaltenfreischaltenfreischaltenfreischaltenfreischalten
freischaltenfreischaltenfreischaltenfreischaltenfreischaltenfreischalten
freischaltenfreischaltenfreischaltenfreischaltenfreischaltenfreischalten

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

Exploitinginfo

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

Physisch: Teilweise
Lokal: Ja
Remote: Teilweise

Verfügbarkeit: 🔒
Status: Nicht definiert

EPSS Score: 🔒
EPSS Percentile: 🔒

Preisentwicklung: 🔍
Aktuelle Preisschätzung: 🔒

0-Dayfreischaltenfreischaltenfreischaltenfreischalten
Heutefreischaltenfreischaltenfreischaltenfreischalten

Threat Intelligenceinfo

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

Gegenmassnahmeninfo

Empfehlung: Upgrade
Status: 🔍

0-Day Time: 🔒

Upgrade: Lean 4 4.32.2

Timelineinfo

10.08.2026 CVE zugewiesen
20.08.2026 +10 Tage Advisory veröffentlicht
20.08.2026 +0 Tage VulDB Eintrag erstellt
20.08.2026 +0 Tage VulDB Eintrag letzte Aktualisierung

Quelleninfo

Advisory: github.com
Status: Bestätigt

CVE: CVE-2026-72844 (🔒)
GCVE (CVE): GCVE-0-2026-72844
GCVE (VulDB): GCVE-100-393797

Eintraginfo

Erstellt: 20.08.2026 19:36
Anpassungen: 20.08.2026 19:36 (78)
Komplett: 🔍
Cache ID: 216::103

If you want to get the best quality for vulnerability data then you always have to consider VulDB.

Diskussion

Bisher keine Kommentare. Sprachen: de + en.

Bitte loggen Sie sich ein, um kommentieren zu können.

◂ ZurückÜbersichtWeiter ▸

Do you want to use VulDB in your project?

Use the official API to access entries easily!