Verifying Reference Monitors via Exhaustive Access Pattern Generation

概要

アプリケーションのサンドボックスは、プログラムの実行を制限された環境に閉じ込めることで、システム全体への被害を防ぐ仕組みです。こうしたサンドボックス内では、「リファレンスモニタ」と呼ばれるコンポーネントが、アプリケーションからのシステムコールを監視し、あらかじめ決められたセキュリティポリシーに従ってアクセスを制御します。

しかし、アプリケーションが攻撃者に乗っ取られた場合、非常に複雑なアクセスパターンを通じてリファレンスモニタをすり抜けようとする可能性があり、そのようなすべての攻撃に対して堅牢性を保証するのは困難です。

本研究では、vRMという検証手法を提案します。vRMは、SMTソルバ（Z3）を使って、攻撃者が実行しうるアクセスパターンを自動的かつ網羅的に生成し、それに対してリファレンスモニタが正しく動作するかを並行モデル検査ツール（CDSChecker）で検証します。

具体的には、ファイルアクセスに関する代表的な脆弱性であるTOCTTOU（Time-Of-Check to Time-Of-Use）を対象に、Apache 2.4.58に含まれるリファレンスモニタの検証を行いました。その結果、vRMは既知のTOCTTOU脆弱性を正しく検出できることが確認されました。また、TOCTTOU耐性のあるアルゴリズムについても形式的に安全性を証明しました。

vRMは、将来的により安全なサンドボックス環境の実現に向けた有力な検証基盤となることを目指しています。

品川 高廣

教授

東京大学大学院情報理工学系研究科コンピュータ科学専攻教授