CVE-2020-37268 — Rocq/Coq Print Assumptions пропускает проверку unsafe-универсумов через Parameter Inline

Обход аудита доказательств через инлайнинг функтора модуля — не исправлено с 2020 года.

Сводка уязвимости

Print Assumptions не сообщает о том, что определение было построено с отключённой проверкой универсумов, когда это определение попадает к вызывающему коду через Parameter Inline в типе модуля. Применение функтора инлайнит тело параметра и отбрасывает запись о контексте Unset Universe Checking, поэтому полученная константа не показывает никаких признаков небезопасной операции.

Таким образом, модуль может использовать противоречие универсумов для доказательства False, а Print Assumptions сообщает о зависимом доказательстве как о замкнутом в глобальном контексте — без аксиом, без видимых флагов небезопасности.

coqchk действительно отвергает полученный скомпилированный файл .vo, но внутрипроцессный аудит допущений (Print Assumptions) не обнаруживает проблему.

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

docker build -t rocq-cve-poc-12155 .
docker run --rm rocq-cve-poc-12155

На уязвимой версии (Rocq 8.11 – 9.2.0 и все Coq 8.x с системой модулей) вывод подтверждает доказательство 0 = 1, при этом Print Assumptions сообщает о нём как о замкнутом.

Влияние

Любой рабочий процесс, полагающийся на Print Assumptions как на единственную проверку целостности, может быть затронут:

• Формально верифицированные компиляторы (CompCert)
• Верифицированные ядра ОС (CertiKOS)
• Фреймворки separation logic (Iris)
• Математические библиотеки (MathComp)
• Proof-carrying code, где вредоносный файл .v в зависимости может внести некорректные объявления, проходящие аудит допущений
• Верифицированные смарт-контракты (ConCert)
• Любой проект, не запускающий регулярно coqchk для скомпилированного вывода

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

Когда тип модуля объявляет Parameter Inline, применение функтора инлайнит тело параметра в вызывающий контекст. Этот инлайнинг отбрасывает метаданные, фиксирующие, что исходное определение было создано в контексте Unset Universe Checking. Поэтому граф универсумов принимает противоречивые ограничения универсумов из инлайненного тела, а Print Assumptions не видит никаких следов небезопасного контекста.

Ошибка открыта с 2020 года (issue Coq #12155) и задокументирована в файле проекта dev/doc/critical-bugs.md. По состоянию на Rocq 9.2.0 исправление не принято.

Оценка

Поле	Значение
CVE	CVE-2020-37268
CVSS 3.1	AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N — 7.1 (High)
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 (Medium)
CWE	CWE-778 — Insufficient Logging

Затронутые версии

Продукт	Затронуты	Исправлено
Coq	8.11 – 8.20	Не исправлено
Rocq Prover	8.20 – 9.2.0	Не исправлено

Меры защиты

• Запускайте coqchk для всех скомпилированных файлов .vo перед тем, как доверять доказательствам в production. coqchk обнаруживает противоречие универсумов, которое пропускает Print Assumptions.
• Проводите аудит зависимостей модулей — атака требует типа модуля с Parameter Inline, скомпилированного в контексте Unset Universe Checking.
• По состоянию на Rocq 9.2.0 исправленная версия недоступна.

Ссылки

Отчёт об ошибке	rocq-prover/rocq#12155
Документ о критических ошибках	dev/doc/critical-bugs.md
Рекомендация VulnCheck	vulncheck.com

Хронология

Дата	Событие
2020	Ошибка обнаружена Jason Gross (coq/coq#12155)
2020–2026	Ошибка остаётся открытой, задокументирована в critical-bugs.md
2026-08-24	CVE-2020-37268 опубликован VulnCheck
2026-08-24	Опубликован воспроизводимый в Docker PoC

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

• Обнаружение ошибки: Jason Gross
• Упаковка PoC: Jonathan Brossard (@endrazine) — MOABI / PSIRT.com