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