CVE-2026-72711 — ошибка корректности ядра Lean 4: отравление кэша вывода

Доказательство 0 = 1 без аксиом путём отравления кэша FVar непрозрачного объявления.

Поле	Значение
Отчёт об ошибке	leanprover/lean4#14484
Исправление	leanprover/lean4#14498
Затронуто	Lean 4 ≤ `v4.31.0` / все предыдущие версии
Исправлено в	nightly 2026-07-23+, перенесено в v4.32.1 и v4.33.0
CVSS 3.1	`AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N` — 7.1
CWE	CWE-488 (Раскрытие элемента данных неверной сессии), CWE-20 (Некорректная проверка входных данных)
CVE	CVE-2026-72711

Краткое описание уязвимости

Путь environment::add_opaque ядра Lean 4 не вызывает check_no_metavar_no_fvar для тела объявления — в отличие от определений и теорем, которые выполняют эту проверку замкнутости перед проверкой типа значения.

Враждебная метапрограмма эксплуатирует это упущение через отравление кэша вывода:

Затравка — Специально сконструированное выражение типа (cachePrimingType) является замкнутой бета-редексой, дефиниционно равной False. Во время проверки его типа ядро создаёт временное локальное объявление _kernel_fresh.2 : False и кэширует его выведенный тип в кэше вывода экземпляра type_checker.
Инвалидация контекста — Локальный контекст восстанавливается (временная переменная удаляется), но кэш вывода сохраняется в том же экземпляре type_checker. Запись кэша теперь устарела — она сопоставляет идентификатор, который больше не ссылается ни на что в области видимости.
Эксплуатация — Значение непрозрачного объявления — это Expr.fvar, указывающий на устаревший идентификатор. Обращение к кэшу срабатывает до того, как ветвь FVar проверит принадлежность локальному контексту, возвращая False в качестве типа без какого-либо обнаружения несвязанной переменной.

Результат — принятая ядром непрозрачная константа типа False, из которой тривиально следует 0 = 1.

Эксплойт:

Использует только проверяемый путь ядра addDecl
Работает с --trust=0 (максимальная проверка)
Сообщает об отсутствии аксиом через #print axioms
Не использует sorry, unsafeCast, debug.skipKernelTC, FFI или подмену .olean
Проходит воспроизведение leanchecker --fresh

Использование

docker build -t lean-cve-poc-14484 .
docker run --rm lean-cve-poc-14484

Ожидаемый вывод на уязвимой версии Lean:

[*] Running CachePoisonFalse.lean with --trust=0 ...
kernel accepted bad : False
'bad' does not depend on any axioms
'assumptionFreeFalse' does not depend on any axioms
'zero_eq_one' does not depend on any axioms

[!] VULNERABILITY CONFIRMED

    zero_eq_one : 0 = 1
    Depends on: no axioms

    Bug class:  Inference cache poisoning (CWE-488)
    Root cause: missing check_no_metavar_no_fvar in add_opaque
    Bug report: https://github.com/leanprover/lean4/issues/14484
    Fix:        https://github.com/leanprover/lean4/pull/14498

В исправленной версии Lean ядро отклоняет некорректно типизированное непрозрачное объявление, и скрипт сообщает, что версия не уязвима.

Влияние

Затронута любая система, которая полагается на проверенные ядром Lean доказательства как на эталонную истину. Это включает:

Формально верифицированное программное обеспечение: компиляторы, криптографические библиотеки, смарт-контракты, авионика, автомобильная электроника — любое обоснование безопасности, построенное на доказательстве Lean, недействительно, если оно построено с использованием затронутой версии.
Код с доказательствами (proof-carrying code): вредоносная зависимость в пакете Lake может незаметно внедрить некорректные объявления, которые использует нижестоящий код.
Независимые проверщики: автор отчёта подтвердил, что воспроизведение через leanchecker --fresh также принимает эксплойт. Формат экспорта comparator не может выразить FVar, поэтому этот путь валидации не затронут.
Доказательства, сгенерированные ИИ: системы вроде AlphaProof, DeepSeek-Prover и Kimina-Prover, использующие Lean как доверенный бэкенд, могут создавать доказательства, эксплуатирующие ошибки ядра, вместо доказательства теорем.

Технические подробности

Первопричина

В src/kernel/environment.cpp функция add_opaque проверяет тип непрозрачного значения, но не выполняет проверку замыкания:

environment environment::add_opaque(declaration const & d, bool check) const {
    scoped_diagnostics diag(*this, check);
    opaque_val const & v = d.to_opaque_val();
    if (check) {
        type_checker checker(*this, diag.get());
        check_constant_val(*this, v.to_constant_val(), checker);
        // ← MISSING: check_no_metavar_no_fvar(*this, v.get_name(), v.get_value());
        expr val_type = checker.check(v.get_value(), v.get_lparams());
        // ...
    }
}

И add_definition, и add_theorem вызывают check_no_metavar_no_fvar для своих значений перед их проверкой типов. Пропуск в add_opaque является точкой входа.

Механизм отравления кэша

Кэш вывода в type_checker сопоставляет выражения с их выведенными типами. В infer_type_core поиск в кэше:

auto it = m_infer_type_cache[binfo_idx(bi)].find(e);
if (it != m_infer_type_cache[binfo_idx(bi)].end())
    return it->second;

срабатывает до того, как ветвь FVar проверит принадлежность к локальному контексту:

case expr_kind::FVar: {
    optional<local_decl> d = m_lctx.find_local_decl(e);
    if (!d) throw_kernel_exception(...);
    return d->get_type();
}

Атакующий управляет заполнением кэша через выражение типа, делая имя устаревшей записи (_kernel_fresh.2) предсказуемым и доступным для атаки.

Сравнение с #14576

Аспект	#14484 (эта ошибка)	#14576
Класс ошибки	Отравление кэша	Путаница типов через валидацию проекции
Точка входа	`add_opaque` без проверки замыкания	Вложенные индуктивные фантомные параметры
Задействован кэш	Да — кэш вывода	Да — сравнение хэшей выражений
Влияет на leanchecker	Да	Да
Влияет на comparator	Нет (FVar невыразим)	Да

Связанные работы

endrazine/lean-cve-poc — PoC для ошибки вложенной индуктивной проекции #14576 (та же структура репозитория)
lean4lean soundness fix — lean4lean был независимо затронут той же ошибкой отравления кэша

Благодарности

Обнаружение ошибки: Patrick Hulin (@phulin), при содействии GPT-5.6 Sol
Исправление ядра: Joachim Breitner (@nomeata), PR #14498
Упаковка PoC: Jonathan Brossard (@endrazine)

lean-cve-poc-14484

Популярное