CVE-2026-72704

요약

Rocq Prover의 가드 검사기는 귀납적 타입 매개변수가 transport에 의해 변경된 후 해당 매개변수의 재귀적 트리 표현을 다시 검사하지 않습니다. fixpoint는 타입 간의 동등성을 따라 재귀 인자에 재작성을 적용할 수 있으며, 가드 검사기는 귀납적 타입이 보존된다는 이유로 이를 허용하지만, 해당 매개변수에 대해 기록된 재귀적 트리는 변경됩니다. 첫 번째를 호출하는 두 번째 fixpoint는 검증 없이 변경된 재귀적 트리를 상속받으므로, 구조적으로 감소하지 않는 호출이 종료하는 것으로 받아들여집니다. 그 결과로 생성된 비종료 정의는 자연수가 자신의 후속자와 같다는 것, 따라서 False를 증명하며, 이로부터 모든 명제가 따라 나옵니다. 이 시연은 univalence로부터 따라 나오며 귀납적 구성의 계산법과 일관되는 두 개의 공리를 사용하므로, 모순은 가정이 아닌 가드 검사에서 비롯됩니다. 수정안이 제안되었으나 병합되지는 않았습니다.

소스

• rocq-cve-poc-22024PoC

  CVE-2026-72704 — Rocq Guard Checker가 전송 후 손상된 재귀 트리를 신뢰함