SMTソルバを用いたアクセスパターンの網羅的生成による参照モニタの容易な形式検証

概要

アプリケーションに対するサンドボックスでは，攻撃者に乗っ取られた場合の不正アクセス被害を最小限に抑えるために，参照モニタと呼ばれるソフトウェアでシステムコールのアクセス制御をおこなう．しかし，攻撃者はアクセス制御を迂回するために極めて複雑なパターンのシステムコールを発行する可能性があり，参照モニタがあらゆるアクセスパターンに対して確実にアクセス制御を実施できることを保証することは難しい．形式検証はソフトウェアの安全性を保証する有効な手法であるが，参照モニタが対応しなければならない全てのアクセスパターンを適切にモデル化することは容易ではない．本論文では，ファイルシステムに対する不正アクセスを対象とした，アクセスパターンの網羅的生成による参照モニタの容易な形式検証手法を提案する．モデルとなるファイルシステムとアクセス制御ポリシーをもとに，Time-of-check to time-of-use（TOCTTOU）などの不正アクセスが起こりうる全ての並行アクセスパターンを SMT ソルバを用いて網羅的に生成し，参照モニタがそれらの不正アクセスを防止できることを並行モデル検査器を用いて検証する．実際に，SMT ソルバの Z3 を用いた並行アクセスパターン生成器と，検査器のための簡易ファイルシステムモデル mockfs を実装し，並行モデル検査器 CDSChecker を用いて参照モニタの形式検証を実施した．その結果，Apache 内蔵の参照モニタに相当するアクセス制御プログラムには TOCTTOU に対する問題があることを確認したほか，既知の TOCTTOU 耐性アルゴリズムを実装した参照モニタに対して，形式検証により実際に TOCTTOU 耐性が保証されていることを確認した．

品川 高廣

教授

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