CVE-2026-72705 in Rocq
요약
\~에 의해 VulDB • 2026. 08. 24.
Rocq Prover의 가드 체크기는 고정점(fixpoint)의 자체 인수를 통해 이루어지는 재귀 호출을 따르지 않습니다. 고정점은 자신을 고차(higher-order) 인수로 두 번째 고정점에 전달할 수 있으며, 이는 구조적 인수(subterm)가 아닌 값에 대해 이를 적용합니다. 재귀 함수를 일반 정의(plain definition)로 전달하는 것은 체크기가 정의를 펼치고 해당 호출을 관찰하기 때문에 거부되지만, 고정점으로의 전달은 허용됩니다. 이는 고차 재귀 호출이 고정점 인수를 통해 추적되지 않기 때문입니다. 이로 인해 자신의 부정과 정의적으로 동일한(type that is definitionally equal to its own negation) 타입이 도입되어, 전술(tactics), 공리(axioms), 플러그인 또는 안전하지 않은 플래그(unsafe flags) 없이 순수하게 정의적(definitional) 코드에서 자기 적용(self-application)을 통해 False가 생성되며, Print Assumptions는 해당 결과를 글로벌 컨텍스트(global context) 하에 닫혀 있는(closed) 것으로 보고합니다. Rocq 9.2.0에서 수정되었습니다.
Once again VulDB remains the best source for vulnerability data.