CVE-2026-72705: Rocq Prover before 9.2.0 Guard Checker Accepts Fixpoint Passed as a Higher-Order Argument
Оценка Noroxi
Приоритет: Наблюдать (оценка срочности 27/100)
- Есть публичный код proof-of-concept (GitHub); записей об эксплуатации в реальных атаках нет.
- Вероятность эксплуатации в ближайшие 30 дней: 0,17% (FIRST EPSS).
- Может быть вызвана пользователем с локальным доступом к системе. Учётная запись или пароль не требуются. Особые условия не требуются; воспроизводится стабильно.
- Исправленная версия не указана, но в ссылках есть исправление (коммит или PR).
Пока низкий приоритет. См. разделы об исправлении и затронутых версиях ниже.
Формируется автоматически по данным записи: CVSS (NVD и CNA), CISA KEV и SSVC, FIRST EPSS, источники эксплойтов, исправленные версии. Как мы считаем
Первоисточники: NVD · CVE.org · FIRST EPSS
The guard checker in Rocq Prover does not follow recursive calls made through a fixpoint's own arguments. A fixpoint may pass itself as a higher-order argument to a second fixpoint, which then applies it to a value that is not a subterm of the structural argument. Passing the recursive function to a plain definition is rejected because the checker unfolds the definition and observes the call, but passing it to a fixpoint is accepted because higher-order recursive calls through fixpoint arguments are not tracked. This admits a type that is definitionally equal to its own negation, so self-application produces False in purely definitional code, without tactics, axioms, plugins or unsafe flags, and Print Assumptions reports the result as closed under the global context. Fixed in Rocq 9.2.0.
- Опубликовано
- 24 авг. 2026 г.
- Обновлено
- 26 окт. 2026 г.
- EPSS
- 0,1 % · 7-й процентиль
- CWE
- CWE-670
Инструменты для отчёта
Оценка срочности
27
Наблюдать
Пока низкий приоритет.
- CVSS
- 27 / 40 · 6.8 / 10
- CISA KEV
- 0 / 30 · Нет в списке
- EPSS
- 0 / 30 · 0,1 %
Решение CISA SSVC
- Эксплуатация
- proof of concept
- Автоматизируемо
- нет
- Техническое влияние
- частичное
Vulnrichment: входные данные дерева решений CISA.
Оценка CNA и NVD
- NVD
- —
- CNA · VulnCheck
- 6,8
- NVD ещё не выставил свою оценку; показана оценка CNA.
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
Оценка присваивающего органа и независимая оценка NVD. Разрыв означает, что критичность спорна.
Узнайте, когда запись изменится
- Нет в KEV: эксплуатация в реальных атаках не зафиксирована
- Есть PoC, боевого модуля нет
- Исправленной версии пока нет
Если что-то из этого изменится, сообщим в ежедневной сводке.
У вас WordPress? Проверьте сайт бесплатно в WP Lens
Анализ Noroxi
Что это значит для вашей инфраструктуры?
Оценка выше формируется автоматически по данным записи и не знает вашей среды. Наша команда проверит на ваших системах, действительно ли уязвимость эксплуатируема и какой меры достаточно.
Мы используем этот продукт, нужна помощьЗатронутые системы
Затронута ли ваша версия?
Выберите продукт и введите свою версию. Она сравнивается с диапазонами этой записи прямо в браузере и никуда не отправляется.
—
Версии, заявленные вендором
Диапазоны затронутых версий, заявленные назначающей организацией (VulnCheck). Не зависят от анализа CPE в NVD и обычно опережают его.
rocq-prover rocq
- до 9.2.0затронута
Тот же продукт
rocq-prover: все записиДругие записи с наивысшей оценкой для того же основного продукта.
- CVE-2026-72714Rocq Prover through 9.2.0 Universe Checking State Desynchronised After Module Close27Наблюдать
- CVE-2026-72704Rocq Prover through 9.2.0 Guard Checker Trusts Corrupted Recursive Tree After Transport27Наблюдать
- CVE-2026-72703Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked Cross-Calls27Наблюдать
Опубликованы до и после этой записи в том же продукте
- ← РаньшеCVE-2020-3726824 авг. 2026 г. · Coq and Rocq Prover Print Assumptions Omits Unsafe Universe Checking Inlined Through Parameter Inline27Наблюдать
Исправление
На какую версию обновиться
Версии с исправлением по данным вендора, реестров пакетов и Microsoft. Перед обновлением сверьтесь с бюллетенем вендора.
Для этой записи не зафиксирована версия с исправлением. Смотрите бюллетени вендора в источниках.
Статус эксплойта
Есть proof of concept
Существует публичный PoC или сигнатура обнаружения. Знание об эксплойте доступно; не откладывайте установку исправлений.
Доказательство
- Репозиторий PoC на GitHub ×1
Noroxi не размещает код эксплойтов и не даёт на них ссылок. Показываются имена модулей Metasploit и идентификаторы шаблонов Nuclei (имена, не код); записи Exploit-DB и репозитории PoC даются только числом.
| Источник | Тип | Дата |
|---|---|---|
| Репозиторий PoC на GitHub | stars:0 | 2026-08-23 |
Контекст для исследователя
Для пентестеров и исследователей: профиль атаки, расхождение оценок, хронология, коммиты исправлений, авторы, кандидаты в варианты и цепочки, охват bug bounty. Всё выводится из имеющихся данных; без кода эксплойтов.
Хронология
От публикации до сегодня: proof of concept, модуль Metasploit, CISA KEV и запись об исправлении. Даты — как сообщают источники.
- Первый PoC-2 дн.
- Публикация
- Сегодня29 окт. 2026 г.+66 дн.
Ежедневная оценка FIRST EPSS; записываются только изменения от 0,01 (ступенчатый график).
Ссылки на патчи и коммиты
Коммиты, PR и diff среди источников. Отправная точка для patch-diff и поиска вариантов; это исправления, не эксплойты.
Авторы
Все исследователиНашедшие, сообщившие и аналитики, названные в записи CNA. Нажмите имя, чтобы увидеть другие записи исследователя.
- Tristan Stérinнашёл
- Jonathan Brossard (MOABI)нашёл
Кандидаты в варианты
Тот же продукт, тот же класс уязвимости, в пределах 18 месяцев. Если патч не закрыл первопричину, родственная ошибка здесь.
- CVE-2026-72703с разницей 0 дн.Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked Cross-Calls27Наблюдать
- CVE-2026-72704с разницей 0 дн.Rocq Prover through 9.2.0 Guard Checker Trusts Corrupted Recursive Tree After Transport27Наблюдать
Кандидаты в цепочки
Обход аутентификации и уязвимость, требующая привилегий, в одном продукте и близко по времени: вместе они могут дать путь без аутентификации.
—
Охват bug bounty
Известной публичной программы нет.
Источник: bounty-targets-data (публичные списки HackerOne, Bugcrowd, Intigriti, YesWeHack).
Технические детали
Условия атаки
- Может быть вызвана пользователем с локальным доступом к системе.
- Учётная запись или пароль не требуются.
- Особые условия не требуются; воспроизводится стабильно.
В случае успеха
- Конфиденциальность
- Целостность
- Доступность
- Вектор атаки
- Локальный
- Сложность атаки
- Низкая
- Требуемые привилегии
- Не требуются
- Взаимодействие с пользователем
- P
- Область действия
- X
Класс уязвимости (CWE)
CWE-670 · Always-Incorrect Control Flow ImplementationВектор CVSS
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
nvd-secondary
Контекст атаки
Шаблоны атак MITRE CAPEC и техники ATT&CK для этого класса уязвимости (CWE). Отправная точка для правил обнаружения и threat hunting.
У MITRE нет сопоставления CAPEC/ATT&CK для этого CWE.
Журнал изменений
- Зрелость эксплойтаnone → poc
Для отслеживаемых записей эти изменения приходят и как уведомления. →
Источники
Показать все источники (ещё 5)Свернуть
Рекомендации вендоров и официальные записи. Ссылки на эксплойты/PoC намеренно исключены.