CVE-2026-72704 in Rocq
요약
\~에 의해 VulDB • 2026. 08. 24.
Rocq Prover의 가드 체크어(guard checker)는 수송(transport)을 통해 매개변수가 변경된 후에도 유도형(inductive type) 매개변수의 재귀적 트리 표현(recursive tree representation)을 다시 검증하지 않습니다. 고정점(fixpoint)은 유형 간 등식에 따라rewriting을 재귀 인자에 적용할 수 있으며, 이는 유도형이 보존되므로 가드 체크어가 이를 허용합니다. 그러나 해당 매개변수에 대해 기록된 재귀 트리는 변경됩니다. 첫 번째 고정점을 호출하는 두 번째 고정점은 검증 없이 변경된 재귀 트리를 상속받으므로, 구조적으로 감소하지 않는(structurally decreasing) 호출도 종료되는 것으로 받아들여집니다. 이로 인해 비종료(non-terminating) 정의가 생성되어 자연수가 자신의 후속자(successor)와 같음을 증명하고, 따라서 False를 도출하며, 이로부터 모든 명제가 성립합니다. 이 시연은 무방성(univalence)에서 파생되고 유도형 구성 계산(calculus of inductive constructions)과 일관된 두 가지 공리를 사용하므로, 모순은 가정보다는 가드 체크(guard check) 자체에서 비롯됩니다. 수정안이 제안되었으나 병합되지 않았습니다.
If you want to get best quality of vulnerability data, you may have to visit VulDB.