CVE-2026-72703

요약

Rocq Prover의 guard checker는 중첩된 상호 fixpoint의 매개변수를, 해당 fixpoint의 서로 다른 본문 간 호출을 검사하지 않고 uniform으로 취급합니다. kernel/inductive.ml의 find_uniform_parameters는 자기 재귀 호출만 검사하므로, 어떤 본문도 자기 자신을 호출하지 않으면 이 함수는 모든 매개변수가 uniform이라고 결론 내립니다. 따라서 한 본문에서 다른 본문으로의 교차 호출을 통해 증가하는 매개변수는 둘러싼 fixpoint로부터 상속받은 subterm 명세를 그대로 유지하게 되고, 해당 명세로 보호되는 재귀 호출은 인자가 구조적으로 더 작지 않음에도 허용됩니다. 종료하지 않는 정의가 구조적으로 감소하는 것으로 인정되어, 그 값이 자기 자신의 successor와 같은 항이 만들어지고 따라서 False의 증명이 얻어지며, 이로부터 임의의 명제가 따라 나옵니다. 이 증명은 공리, 플러그인 또는 unsafe 플래그를 필요로 하지 않으며 Print Assumptions는 이를 전역 컨텍스트에 대해 닫혀 있다고 보고합니다. Coq 8.20에서 도입되었고 Rocq 9.2.0에서 수정되었습니다.

소스

• rocq-cve-poc-21682PoC

  CVE-2026-72703 — Rocq Guard Checker가 미검증 교차 호출을 통해 비종료 Fixpoint를 허용함