| Research Abstract |
(1)再帰的プログラムのモデル検査に関する研究.
(a)我々が以前より取り組んでいる,実行履歴に基づくアクセス制御付きプログラム(HBACプログラム)の安全性検証法において,種々の最適化を行うことにより,高速な検証が可能であることを実証した.我々のモデル検査アルゴリズムでは,検証対象のプログラムに対するモデル検査問題を,文脈自由文法(CFG)の空判定問題に帰着しており,一般にアクセス権の個数に対して指数的な検証時間を要する.そこで,CFGを構成する際,uselessな規則(開始記号から到達しないか,または,終端記号列を一つも生成しない規則)の構成を防ぐ最適化法を提案した.Chinese-Wallポリシとオンラインバンキングシステムの2つの例題について最適化の効果を実測した結果,どちらの検証例においても,最適化を行わない場合,アクセス権の数が5個程度までしか検証できなかったのに対し,最適化を行うことにより,前者の例ではアクセス権の数が80個のとき約64秒,後者の例では60個のとき約0.O1秒で検証を行えた.
(b)プログラムの実行による情報流出を解析する手法として情報フロー解析が有効である.本研究では,HBACプログラムに対し,モデル検査に基づく新しい情報フロー解析法を提案した.提案手法を用いることにより,プログラムの実行完了時に出力の機密度(security class, SC)がどのようになるかだけでなく,「SCがτであるような値を引数として関数fが呼び出されたならば,いっかSCがτ'である値を引数として関数gが呼び出される」のような,実行系列上に拡張された情報フローに関する性質を調べることができる.
(2)実行履歴に基づくアスペクト折込み機能の形式モデル:Aspect-J等で採用されているPA (pointcut and advice)の形式モデルA-LTSを提案した.A-LTSと既存の計算モデルの表現能力を比較した結果,A-LTSの受理言語,決定性文脈自由言語,線形文脈自由言語のクラスはすべて互いに他を含まないことを証明した.その系として,A-LTSにはプッシュダウンシステムのモデル検査法が適用可能であることがわかった.
|
