CVE-2026-72705
Rocq Prover до 9.2.0: проверка защиты принимает fixpoint, переданный как аргумент высшего порядка
- Опубликовано
- 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, воздействием и вашей средой.
Резюме
Проверщик guard в Rocq Prover не отслеживает рекурсивные вызовы, выполняемые через собственные аргументы fixpoint. Fixpoint может передать себя в качестве аргумента высшего порядка второму fixpoint, который затем применяет его к значению, не являющемуся подтермом структурного аргумента. Передача рекурсивной функции в обычное определение отклоняется, поскольку проверщик разворачивает определение и обнаруживает вызов, но передача её в fixpoint принимается, так как рекурсивные вызовы высшего порядка через аргументы fixpoint не отслеживаются. Это допускает тип, дефиниционно равный собственному отрицанию, поэтому самоприменение порождает False в чисто дефиниционном коде, без тактик, аксиом, плагинов или небезопасных флагов, а Print Assumptions сообщает о результате как о замкнутом в глобальном контексте. Исправлено в Rocq 9.2.0.
Источники
CVE-2026-72705 — Rocq Guard Checker принимает fixpoint, переданный как аргумент высшего порядка
Ответственное использование
Используйте информацию об уязвимостях только в тех системах, которыми вы владеете или имеете право тестировать. Kitploit ссылается на метаданные общедоступных исследований и не хранит код эксплойта или вредоносные полезные данные.