endrazine/rocq-cve-poc-12155CVE-2020-37268 — Rocq/Coq Print Assumptions가 Parameter Inline을 통한 안전하지 않은 Universe 검사 누락
모듈 펑터 인라이닝을 통한 증명 감사 우회 — 2020년 이후 미수정.
Print Assumptions는 정의가 모듈 타입의 Parameter Inline을 통해 호출자에게 도달할 때 해당 정의가 유니버스 검사가 비활성화된 상태에서 구축되었음을 보고하지 못합니다. 펑터 적용은 매개변수의 본문을 인라이닝하고 Unset Universe Checking 컨텍스트의 기록을 삭제하므로, 결과 상수는 안전하지 않은 작업의 흔적을 전혀 보여주지 않습니다.
따라서 모듈은 유니버스 불일치를 사용하여 False를 증명할 수 있으며, Print Assumptions는 종속 증명을 전역 컨텍스트 하에서 닫혀 있는 것으로 보고합니다 — 공리도 없고, 안전하지 않은 플래그도 보이지 않습니다.
coqchk는 결과로 생성된 컴파일된 .vo 파일을 거부하지만, 프로세스 내 가정 감사(Print Assumptions)는 이 문제를 잡아내지 못합니다.
docker build -t rocq-cve-poc-12155 .
docker run --rm rocq-cve-poc-12155
취약한 버전(Rocq 8.11 – 9.2.0, 그리고 모듈 시스템을 갖춘 모든 Coq 8.x)에서는 출력이 0 = 1의 증명을 확인하며, Print Assumptions는 이를 닫혀 있는 것으로 보고합니다.
Print Assumptions를 유일한 무결성 검사로 의존하는 모든 워크플로가 영향을 받을 수 있습니다:
.v 파일이 가정 감사를 통과하는 불건전한 선언을 도입할 수 있는 증명 운반 코드coqchk를 정기적으로 실행하지 않는 모든 프로젝트모듈 타입이 Parameter Inline을 선언하면, 펑터 적용은 매개변수의 본문을 호출 컨텍스트로 인라이닝합니다. 이 인라이닝은 원래 정의가 Unset Universe Checking 하에서 생성되었음을 기록한 메타데이터를 폐기합니다. 따라서 유니버스 그래프는 인라이닝된 본문으로부터 일관성 없는 유니버스 제약을 받아들이고, Print Assumptions는 안전하지 않은 컨텍스트의 흔적을 전혀 보지 못합니다.
이 버그는 2020년(Coq 이슈 #12155)부터 열려 있으며 프로젝트의 dev/doc/critical-bugs.md에 문서화되어 있습니다. Rocq 9.2.0 기준으로 수정 사항이 병합되지 않았습니다.
| 필드 | 값 |
|---|---|
| CVE | CVE-2020-37268 |
| CVSS 3.1 | AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N — 7.1 (높음) |
| CVSS 4.0 | AV:L/AC:L/AT:N/PR:N/UI:P/VC:N/VI:H/VA:N/SC:N/SI:N/SA:N — 6.8 (중간) |
| CWE | CWE-778 — 불충분한 로깅 |
| 제품 | 영향 받음 | 수정됨 |
|---|---|---|
| Coq | 8.11 – 8.20 | 미수정 |
| Rocq Prover | 8.20 – 9.2.0 | 미수정 |
.vo 파일에 대해 coqchk를 실행하십시오. coqchk는 Print Assumptions가 놓치는 유니버스 불일치를 잡아냅니다.Unset Universe Checking 하에서 컴파일된 Parameter Inline을 가진 모듈 타입을 필요로 합니다.| 버그 보고서 | rocq-prover/rocq#12155 |
| 치명적 버그 문서 | dev/doc/critical-bugs.md |
| VulnCheck 권고 | vulncheck.com |
| 날짜 | 사건 |
|---|---|
| 2020 | Jason Gross가 버그 보고 (coq/coq#12155) |
| 2020–2026 | 버그가 열린 상태로 유지되며 critical-bugs.md에 문서화됨 |
| 2026-08-24 | VulnCheck가 CVE-2020-37268 게시 |
| 2026-08-24 | Docker로 재현 가능한 PoC 게시 |