2007 Fiscal Year Annual Research Report
無限状態モデル検査を用いた高信頼性ソフトウェアの自動検証に関する研究
| Project/Area Number |
18500023
|
|---|
| Research Institution | Nara Institute of Science and Technology |
|---|
Principal Investigator |
関 浩之 Nara Institute of Science and Technology, 情報科学研究科, 教授 (80196948)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
高田 喜朗 高知工科大学, 工学部, 講師 (60294279)
|
|---|
| Keywords | 形式的検証 / モデル検査 / 静的解析 / 形式言語 / アクセス制御 / セキュリティ / 実行履歴 / ソフトウェア学 |
|---|
| Research Abstract |
(1)情報フロー解析
(a)HBAC情報フロー解析:昨年度、実行履歴に基づくアクセス制御付プログラムHBAC(History-Based Access Control)に対するモデル検査器を実装し、その有効性を実証した。今年度はこのモデル検査法を応用した情報フロー解析を開発した。情報フロー解析を行うことにより、「望ましくない情報漏えいが生じない」という意味でアクセス制御が意図通りに機能しているかどうかを確認できる。従来の情報フロー解析法では主にメソッドの入出力間の情報フロー関係を解析していた。これに対して我々は、モデル検査法を応用することにより、一般の実行系列上に拡張された情報フロー解析を行う手法を提案することができた。
(b)最近、自己合成法と呼ばれる情報フロー解析法が提案されている。これは解析精度が従来の型推論に基づく解析法より精度がよいという特長をもつ。本研究では、自己合成法を一般の再帰プログラムに適用できるように拡張した。
(2)実行履歴に基づくアクセス制御モデルの表現能力の比較:Schneiderのセキュリティオートマトン、Fongの狭履歴オートマトン、スタック検査、IIBACをアクセス制御機構にもつプログラムの表現能力を比較した。
(3)その他:上記(1)の言語理論ベースの手法を用いて、以下のような研究成果を挙げた。
(a)等式系と書換え系を内部に演繹系としてもつ木オートマトンの諸性質を明らかにし、XML文書処理への応用についても考察した。
(b)公開木戦略(DTS)とよばれる信用交渉戦略が知られている。文脈自由文法(CFG)によるモデル化を用いてDTSの計算量を明らかにし、妥当な前提条件のもとで効率良く動作するDTS実行アルゴリズムを示した。
(c)CFGの構文解析法を応用し、相互作用をもつRNAの2次構造予測法を提案した。
|
