CVE-2026-72714

요약

Rocq Prover는 유니버스 검사를 로컬에서 비활성화한 모듈이 닫힐 때 유니버스 그래프가 보유한 유니버스 검사 플래그의 사본을 복원하지 않습니다. 모듈 내부에서의 로컬 `Unset Universe Checking`은 모듈이 끝날 때까지만 지속되어야 하며 전역 플래그는 복원되지만, 유니버스 그래프는 자체 사본을 유지하는데 이는 비활성화된 채로 남습니다. 그러면 두 관점이 서로 불일치하게 됩니다. `Test Universe Checking`은 검사를 활성화된 것으로 보고하지만, 커널은 계속해서 유니버스와 일관되지 않는 항을 받아들입니다. 두 유니버스 사이의 제약이 더 이상 강제되지 않으므로 Hurkens의 역설이 적용되어 `False`의 증명을 얻게 되며, 이로부터 어떤 명제든 따라 나옵니다. 이 증명은 모듈이 닫힌 후에는 공리, 플러그인 또는 안전하지 않은 기능을 사용하지 않으며, `Print Assumptions`는 이를 전역 컨텍스트에서 닫힌 것으로 보고하므로, 가정 감사나 플래그 조회 어느 것도 실제 커널 상태를 반영하지 못합니다. 사용 가능한 수정 사항은 없습니다.

소스

• rocq-cve-poc-22287PoC

  CVE-2026-72714 — 모듈 닫힌 후 Rocq 유니버스 검사 상태 동기화 해제