実行履歴に基づくアクセス制御付きプログラムのモデル検査法による情報フロー解析

概要

論文の詳細を見る
プログラム実行系に汎用のアクセス制御機構を導入する試みが注目されている.そのような機構を使ったアクセス制御付きプログラムにおいて,プログラムに織り込んだアクセス制御実行文が目的を達成しているかどうかを確認するための手段として,情報フロー解析が有用であると考えられる.しかし,アクセス制御付きプログラムに対する情報フロー解析法はあまり研究されてこなかった.本稿では,Javaのアクセス制御機構の拡張である履歴に基づくアクセス制御(HBAC)を使ったプログラムに対し,モデル検査に基づく新しい情報フロー解析法を提案する.モデル検査を用いて情報フロー解析を行うことにより,プログラムの実行完了時に出力の機密度(security calss, SC)がどのようになるかだけでなく,「SCがγであるような値を引数として関数fが呼び出されたならば,いつかSCがγ^fである値を引数として関数gが呼び出される.」のような,実行系列上に拡張された情報フローに関する性質を調べることができる.
2007-01-25