CVE-2026-72714
Rocq Prover до версии 9.2.0: рассинхронизация состояния проверки вселенной после закрытия модуля
- Опубликовано
- 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, воздействием и вашей средой.
Резюме
Rocq Prover не восстанавливает копию флага проверки вселенных в графе вселенных, когда закрывается модуль, локально отключивший эту проверку. Локальный `Unset Universe Checking` внутри модуля должен действовать только до завершения модуля, и глобальный флаг восстанавливается, но граф вселенных хранит собственную копию, которая остаётся отключённой. Два представления затем расходятся: `Test Universe Checking` сообщает, что проверка включена, тогда как ядро продолжает принимать термы, несовместимые с вселенными. Поскольку ограничение между двумя вселенными больше не соблюдается, применяется парадокс Хуркенса и даёт доказательство `False`, из которого следует любое утверждение. Доказательство не использует аксиом, плагинов или небезопасных возможностей после закрытия модуля, и `Print Assumptions` сообщает о нём как о замкнутом в глобальном контексте, поэтому ни аудит предположений, ни запрос флага не отражают фактическое состояние ядра. Исправление недоступно.
Источники
CVE-2026-72714 — рассинхронизация состояния проверки вселенной Rocq после закрытия модуля
Ответственное использование
Используйте информацию об уязвимостях только в тех системах, которыми вы владеете или имеете право тестировать. Kitploit ссылается на метаданные общедоступных исследований и не хранит код эксплойта или вредоносные полезные данные.