endrazine/lean-cve-pocCVE-2026-72844 : Пример доказательства "0 = 1" с использованием уязвимости в ядре Lean 4.
Доказательство 0 = 1 без аксиом через обход проверки проекции вложенного индуктивного типа.
| Поле | Значение |
|---|
| CVE | CVE-2026-72844 |
| Уведомление | VulnCheck VCSA |
| Отчёт об ошибке | leanprover/lean4#14576 |
| Исправление | leanprover/lean4#14577 |
| Затронуто | Lean 4 ≤ v4.31.0 / nightly ≤ 2026-07-27 |
| Исправлено в | nightly 2026-07-29+ / v4.32.2 |
| 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 — 6.8 СРЕДНИЙ |
| CVSS 3.1 | AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N — 6.3 СРЕДНИЙ |
| CWE | CWE-843 (Путаница типов) |
Ядро Lean 4 не проверяет, что структура, указанная в выражении проекции,
соответствует типу проецируемого значения, а функция
environment::add_inductive в src/kernel/inductive.cpp не выполняла
проверку типов вложенных индуктивных применений, которые заменяются
вспомогательными типами, поэтому их параметрические аргументы не проходили проверку.
Метапрограмма, работающая в процессе Lean, может зарегистрировать
неправильно типизированный вложенный индуктив, конструктор которого применяет
проекцию .proj C 0 к значению несвязанного типа W, и ядро принимает
объявление через обычный проверяемый путь addDecl при максимальной проверке
ядра. В результате возникает путаница типов, дающая доказательство False
без каких-либо аксиом, из которого можно вывести любое утверждение — включая 0 = 1.
Эксплойт:
addDecl--trust=0 (максимальная проверка)#print axioms показывает отсутствие аксиомsorry, unsafeCast, debug.skipKernelTC, FFI или подмену .oleandocker build -t lean-cve-poc .
docker run --rm lean-cve-poc
Ожидаемый вывод на уязвимой версии Lean:
[*] Running ZeroEqOne.lean with --trust=0 ...
'bad' does not depend on any axioms
'boom' does not depend on any axioms
'zero_eq_one' does not depend on any axioms
zero_eq_one : 0 = 1
[!] VULNERABILITY CONFIRMED — CVE-2026-72844
zero_eq_one : 0 = 1
Depends on: no axioms
На исправленной версии Lean ядро отклоняет неправильно типизированный индуктив, и скрипт сообщает, что версия не уязвима.
Затронуты любые системы, которые доверяют проверенным ядром доказательствам Lean как истине в последней инстанции. Это включает:
Корневая причина кроется в обработке ядром вложенных индуктивных типов.
При исключении вложенного вхождения I Ds is ядро должно проверить,
что параметрические аргументы Ds соответствуют объявленным параметрам
индуктивного типа. Уязвимый код не проверяет, что выражения проекций (.proj)
в Ds ссылаются на правильное имя структуры: .proj C 0 w принимается даже
когда w : W и W ≠ C.
В сочетании с коллизией хеша (ядро использует сравнения Expr.hash
при проверке дефиниционального равенства) это позволяет атакующему
регистрировать объявления, в которых внутреннее присваивание типов ядра
расходится с фактической семантикой терма, что приводит к путанице типов
и доказательству False.