Toward Efficient Formal Verification of Reference Monitors for Isolated Execution

概要

クラウドコンピューティングの進展により、サンドボックスやTEEなどの隔離実行環境によるセキュリティの強化が重要になっています。 しかし、隔離実行環境はOSカーネルやハイパーバイザーなどの信頼されたコンピューティング基盤（TCB）に依存しており、システムソフトウェアの複雑化が進むにつれて、それ自体の安全性の保証が難しくなっています。 この問題に対処するため、我々のアプローチは、セキュリティに重要なコンポーネント、特にリファレンスモニタに焦点を当てています。 リファレンスモニタは、隔離実行環境とTCBシステムソフトウェア間のインターフェースで動作して攻撃者からの入力を直接扱うため、形式検証によってその部分のセキュリティを重点的に強化することはコストパフォーマンスの良いアプローチであると言えます。 しかし、リファレンスモニタを形式検証するためには、その挙動をモデル化する必要がありますが、リファレンスモニタに対する入力や実現するセキュリティポリシーは多岐に渡るため、全てのパターンを網羅することは難しく、その形式検証は容易ではありません。 本研究では、このアプローチにおける最初のステップとして、システムコールレベルのリファレンスモニタを対象として、特にシステムコールの監視中に発生する時差攻撃（TOCTTOU）に対する挑戦を克服することを目指します。 具体的には、自動検証コード生成と並列検証を用いた二段階の徹底的な検証を導入することで、リファレンスモニターが任意のタイミングと順序で発行されるシステムコールに対して、与えられたセキュリティポリシーを正しく実施できることを確認することを目指しています。

品川 高廣

教授

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