CVE-2020-37268

概要

Print Assumptions は、モジュール型内の Parameter Inline を通じて呼び出し元に到達する定義が、universe checking を無効にして生成されたものであることを報告しません。ファンクタを適用するとパラメータの本体がインライン化されますが、そのインライン化によって、その項が Unset Universe Checking の下で構築されたという記録が失われるため、結果として得られる定数には安全でない操作の痕跡が残りません。したがって、モジュール実装は universe の不整合を利用して False を証明し、それをインライン化されたパラメータを通じて公開し、Print Assumptions にその依存する証明がグローバルコンテキストの下で閉じていると報告させることができます。Print Assumptions は、開発が予期しない前提に依存していないことを確認するために用いられるインプロセス監査であるため、この方法で構築された依存関係は、任意の命題を証明しつつその監査を通過します。スタンドアロンのチェッカー coqchk は、結果として得られるコンパイル済みファイルを確かに拒否します。プロジェクトはこの問題を dev/doc/critical-bugs.md の未修正バグとして記録しており、coqchk を使用しない場合のリスクを中程度と評価しています。

ソース

• rocq-cve-poc-12155PoC

  CVE-2020-37268 — Rocq/CoqのPrint Assumptionsはパラメータのインライン化により安全でない宇宙（Universe）チェックを省略する