Куда я попал?
SECURITM это SGRC система, ? автоматизирующая процессы в службах информационной безопасности. SECURITM помогает построить и управлять ИСПДн, КИИ, ГИС, СМИБ/СУИБ, банковскими системами защиты.
А еще SECURITM это место для обмена опытом и наработками для служб безопасности.

CVE-2026-72844

PUBLISHED 21.08.2026

CNA: VulnCheck

Lean 4 Kernel Type Checking Bypass via Mismatched Structure Projections

Обновлено: 21.08.2026
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.

CWE

Идентификатор Описание
CWE-843 The product allocates or initializes a resource such as a pointer, object, or variable using one type, but it later accesses that resource using a type that is incompatible with the original type.

CVSS

Оценка Severity Версия Базовый вектор
6.3 MEDIUM 3.1 CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N
6.8 MEDIUM 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

EPSS

Вероятность Severity Процентиль ? Дата расчёта
0.18% LOW 7.98 30.08.2026

Доп. Информация

Product Status

lean4
Product: lean4
Vendor: leanprover
Default status: unaffected
Версии:
Затронутые версии Статус
Наблюдалось в версиях от 0 до 4.32.2 affected
Наблюдалось в версии 4.32.2 unaffected
Наблюдалось в версии 4.33.0-rc1 affected
 

Ссылки

CISA ADP Vulnrichment

Обновлено: 21.08.2026
Этот блок содержит дополнительную информацию, предоставленную программой CVE для этой уязвимости.

SSVC

Exploitation Automatable Technical Impact Версия Дата доступа
poc no partial 2.0.3 21.08.2026

Мы используем cookie-файлы, чтобы получить статистику, которая помогает нам улучшить сервис для вас с целью персонализации сервисов и предложений. Вы может прочитать подробнее о cookie-файлах или изменить настройки браузера. Продолжая пользоваться сайтом, вы даёте согласие на использование ваших cookie-файлов и соглашаетесь с Политикой обработки персональных данных.