Instituto Nacional de ciberseguridad. Sección Incibe
Instituto Nacional de Ciberseguridad. Sección INCIBE-CERT

017 - Ir a la línea de ayuda en Ciberseguridad    Ir a Agenda     Ir a Sala de prensa     Ir a suscripción de boletines

Vulnerabilidad en lean4 de leanprover (CVE-2026-72844)

Gravedad CVSS v4.0:
MEDIA
Tipo:
No Disponible / Otro tipo
Fecha de publicación:
20/08/2026
Última modificación:
26/10/2026

Descripción

El kernel de Lean 4 no verifica que la estructura nombrada en una expresión de proyección coincida con el tipo del valor que se está proyectando, y environment::add_inductive en src/kernel/inductive.cpp no comprobó el tipo de las aplicaciones inductivas anidadas que son reemplazadas por tipos auxiliares, por lo que sus argumentos paramétricos escaparon a la verificación. Un metaprograma ejecutándose en el proceso de Lean puede registrar un inductivo anidado mal tipado cuyo constructor aplica una proyección .proj C 0 a un valor del tipo no relacionado W, y el kernel admite la declaración a través de la ruta addDecl comprobada ordinaria con la máxima verificación del kernel, sin sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, FFI, o un archivo .olean modificado. El resultado es una confusión de tipos que produce una prueba de Falso que no conlleva axiomas, de la cual se puede derivar cualquier proposición. La prueba de concepto publicada además rellena dos expresiones hasta que sus hashes y profundidades aproximadas colisionan, lo que anula el almacenamiento en caché del kernel; esa es la técnica utilizada para alcanzar la falla, no su causa. La explotación requiere ejecutar un metaprograma en proceso, por ejemplo, construyendo un proyecto o importando una dependencia maliciosa de Lake.

Impacto

Vector 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 CVSS v4.0 Severidad y Métricas:

Puntuación base: 6.80 MEDIA
Vector: 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

Vector de acceso (AV): Local
Complejidad de acceso (AC): Bajo
Attack Requirements (AT): Ninguno
Privilegios Requeridos (PR): Ninguno
Interacción del usuario (UI): Passsive
Confidentiality (VC): Ninguno
Integrity (VI): Alto
Availability (VA): Ninguno
Confidentiality (SC): Ninguno
Integrity (SI): Ninguno
Availability (SA): Ninguno

Puntuación base 4.0
6.80
Gravedad 4.0
MEDIA
Vector 3.x
CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N CVSS v3.1 Severidad y Métricas:

Puntuación base: 6.30 MEDIA
Vector: CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N

Vector de acceso (AV): Local
Complejidad de acceso (AC): Bajo
Privilegios Requeridos (PR): Ninguno
Interacción del usuario (UI): Obligatorio
Alcance (S): Modificado
Impacto a la confidencialidad (C): Ninguno
Impacto a la integridad (I): Alto
Impacto a la disponibilidad (A): Ninguno

Puntuación base 3.x
6.30
Gravedad 3.x
MEDIA

Referencias a soluciones, herramientas e información