CVE-2026-72703 in Rocq
Сводка
по VulDB • 24.08.2026
Проверка guard checker в Rocq Prover считает параметр во вложенной взаимно рекурсивной функции (mutual fixpoint) униформным, не анализируя вызовы между различными телами этой функции. Функция find_uniform_parameters в kernel/inductive.ml проверяет только само-рекурсивные вызовы; поэтому, когда ни одно тело не вызывает себя напрямую, функция заключает, что все параметры являются униформными. Параметр, который увеличивается при кросс-вызове из одного тела в другое, сохраняет спецификацию подтерма (subterm specification), унаследованную от окружающей функции fixpoint, и рекурсивный вызов, защищенный этой спецификацией, принимается, хотя аргумент не является структурно меньшим. Непрерывающееся определение признается как структурно убывающее, что приводит к терму, значение которого равно своему собственному преемнику (successor), и, следовательно, к доказательству False, из которого следует любое утверждение. Это доказательство не требует аксиом, плагинов или небезопасных флагов; команда Print Assumptions сообщает о нем как об закрытом в глобальном контексте. Введено в Coq 8.20 и исправлено в Rocq 9.2.0.
If you want to get the best quality for vulnerability data then you always have to consider VulDB.