CVE-2020-37268
Coq и Rocq Prover Print Assumptions опускает небезопасную проверку вселенных, встроенную через параметр inline
- Опубликовано
- 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 %
- Дата модели
- 27 окт. 2026 г.
EPSS – это статистическая оценка, а не достоверность или мера воздействия. Объедините это с CVSS, статусом KEV, воздействием и вашей средой.
Резюме
Print Assumptions не сообщает, что определение было создано при отключённой проверке вселенных, если это определение попадает к вызывающему через Parameter Inline в типе модуля. Применение функтора встраивает тело параметра, и встраивание отбрасывает запись о том, что терм был построен при Unset Universe Checking, поэтому результирующая константа не несёт следов небезопасной операции. Таким образом, реализация модуля может доказать False с помощью несовместимости вселенных, раскрыть это через встроенный параметр, и Print Assumptions сообщит о зависимом доказательстве как о замкнутом в глобальном контексте. Поскольку Print Assumptions — это внутрипроцессный аудит, используемый для подтверждения того, что разработка не опирается на неожиданные допущения, зависимость, построенная таким образом, проходит этот аудит, доказывая при этом произвольные утверждения. Автономный проверщик coqchk действительно отвергает полученный скомпилированный файл. Проект фиксирует это в dev/doc/critical-bugs.md в разделе неисправленных ошибок и оценивает риск как умеренный, когда coqchk не используется.
Источники
CVE-2020-37268 — Rocq/Coq Print Assumptions пропускает проверку небезопасных вселенных через Parameter Inline
Ответственное использование
Используйте информацию об уязвимостях только в тех системах, которыми вы владеете или имеете право тестировать. Kitploit ссылается на метаданные общедоступных исследований и не хранит код эксплойта или вредоносные полезные данные.