CVE-2020-37268

요약

Print Assumptions는 모듈 타입에서 Parameter Inline을 통해 호출자에게 도달하는 정의가 유니버스 검사가 비활성화된 상태에서 생성되었음을 보고하지 않는다. 펑터를 적용하면 매개변수의 본문이 인라인되며, 인라이닝 과정에서 해당 항이 Unset Universe Checking 하에 구축되었다는 기록이 삭제되므로, 결과 상수에는 안전하지 않은 작업의 흔적이 남지 않는다. 따라서 모듈 구현은 유니버스 불일치를 이용해 False를 증명하고, 이를 인라인된 매개변수를 통해 노출시킨 뒤, Print Assumptions가 해당 의존적 증명을 전역 컨텍스트에 대해 닫혀 있는 것으로 보고하도록 할 수 있다. Print Assumptions는 개발이 예상치 못한 가정에 의존하지 않음을 확인하는 데 사용되는 인프로세스 감사이므로, 이런 방식으로 구축된 의존성은 임의의 명제를 증명하면서도 해당 감사를 통과한다. 독립 실행형 검사기인 coqchk는 결과로 생성된 컴파일된 파일을 거부한다. 프로젝트는 이를 dev/doc/critical-bugs.md의 미수정 버그 항목에 기록하고 있으며, coqchk를 사용하지 않는 경우 위험도를 보통으로 평가한다.

소스

• rocq-cve-poc-12155PoC

  CVE-2020-37268 — Rocq/Coq Print Assumptions가 Parameter Inline을 통한 안전하지 않은 Universe 검사 누락