CVE-2026-72703

Резюме

Проверка guard в Rocq Prover рассматривает параметр вложенного взаимного fixpoint как uniform, не исследуя вызовы между различными телами этого fixpoint. Функция find_uniform_parameters в kernel/inductive.ml проверяет только самовызовы, поэтому, когда ни одно тело не вызывает само себя, функция заключает, что каждый параметр является uniform. Параметр, который растёт через перекрёстный вызов из одного тела в другое, таким образом сохраняет спецификацию subterm, унаследованную от охватывающего fixpoint, и рекурсивный вызов, защищённый этой спецификацией, принимается, хотя аргумент не является структурно меньшим. Не завершающееся определение допускается как структурно убывающее, что даёт терм, значение которого равно своему собственному последователю, и, следовательно, доказательство False, из которого следует любое утверждение. Доказательство не требует аксиом, плагинов или небезопасных флагов, и Print Assumptions сообщает, что оно замкнуто в глобальном контексте. Введено в Coq 8.20 и исправлено в Rocq 9.2.0.

Источники

• rocq-cve-poc-21682PoC

  CVE-2026-72703 — Rocq Guard Checker принимает незавершающийся fixpoint через непроверенные перекрёстные вызовы