CVE-2026-72844
Обход проверки типов ядра Lean 4 через несовпадающие проекции структур
- Опубликовано
- 20 авг. 2026 г.
- Обновлено
- 20 авг. 2026 г.
- Назначение CNA
- VulnCheck
- Наблюдены доказательства
- 24 авг. 2026 г.
Первичный 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:XНизкий · следующие 30 дней
- Процентиль
- 8,2 %
- Дата модели
- 21 сент. 2026 г.
EPSS – это статистическая оценка, а не достоверность или мера воздействия. Объедините это с CVSS, статусом KEV, воздействием и вашей средой.
Резюме
Ядро Lean 4 не проверяет, что структура, указанная в выражении проекции, соответствует типу проецируемого значения, а environment::add_inductive в src/kernel/inductive.cpp не проверял типы вложенных индуктивных применений, которые заменяются вспомогательными типами, поэтому их параметрические аргументы ускользали от проверки. Метапрограмма, работающая в процессе Lean, может зарегистрировать плохо типизированный вложенный индуктивный тип, конструктор которого применяет проекцию .proj C 0 к значению несвязанного типа W, и ядро принимает объявление через обычный проверяемый путь addDecl при максимальном уровне проверки ядра, без sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, FFI или изменённого файла .olean. Результатом является путаница типов, дающая доказательство False без аксиом, из которого можно вывести любое утверждение. Опубликованный proof of concept дополнительно дополняет два выражения до совпадения их хэшей и приблизительных глубин, что обходит кэширование ядра; это метод, использованный для достижения уязвимости, а не её причина. Для эксплуатации требуется запуск метапрограммы в процессе, например, при сборке проекта или импорте вредоносной зависимости Lake.
Источники
1- lean-cve-pocPoC
CVE-2026-72844 : Пример доказательства "0 = 1" с использованием уязвимости в ядре Lean 4.
Ответственное использование
Используйте информацию об уязвимостях только в тех системах, которыми вы владеете или имеете право тестировать. Kitploit ссылается на метаданные общедоступных исследований и не хранит код эксплойта или вредоносные полезные данные.