CVE-2026-72711
Lean 4 до 4.32.2: ядро принимает непрозрачное объявление со свободной переменной без привязки
- Опубликовано
- 24 авг. 2026 г.
- Обновлено
- 26 окт. 2026 г.
- Назначение CNA
- VulnCheck
- Наблюдены доказательства
- 26 окт. 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 дней
- Процентиль
- 7,1 %
- Дата модели
- 25 окт. 2026 г.
EPSS – это статистическая оценка, а не достоверность или мера воздействия. Объедините это с CVSS, статусом KEV, воздействием и вашей средой.
Резюме
Ядро Lean 4 не проверяет, что тело opaque-объявления замкнуто. `environment::add_opaque` опускает вызов `check_no_metavar_no_fvar`, который выполняют пути определения и теоремы, поэтому значение, содержащее свободную переменную, отсутствующую в локальном контексте, не отвергается сразу. Метапрограмма может сначала заставить ядро создать временную локальную переменную типа `False` и записать её тип в кэш вывода средства проверки типов, затем восстановить локальный контекст, пока эта запись кэша сохраняется в том же экземпляре средства проверки типов, и наконец отправить opaque-объявление, значением которого является теперь несвязанная переменная. Поиск в кэше отвечает раньше ветви, которая проверяла бы принадлежность локальному контексту, поэтому ядро выводит кэшированный тип и допускает opaque-константу типа `False`, из которой следует любое утверждение. Объявление принимается через обычный проверяемый путь при максимальном уровне проверки ядра, без `sorry`, `unsafeCast`, `debug.skipKernelTC`, `addDeclWithoutChecking`, внешнего кода или изменённого файла `.olean`, и результат не несёт аксиом. Исправлено в 4.32.2 добавлением недостающей проверки замкнутости.
Источники
CVE-2026-72711 — Ошибка корректности ядра Lean 4: отравление кэша вывода
Ответственное использование
Используйте информацию об уязвимостях только в тех системах, которыми вы владеете или имеете право тестировать. Kitploit ссылается на метаданные общедоступных исследований и не хранит код эксплойта или вредоносные полезные данные.