| 研究課題/領域番号 |
18500023
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
ソフトウエア
|
|---|
| 研究機関 | 奈良先端科学技術大学院大学 |
|---|
研究代表者 |
関 浩之 奈良先端科学技術大学院大学, 情報科学研究科, 教授 (80196948)
|
|---|
| 研究分担者 |
高田 喜朗 高知工科大学, 工学部, 講師 (60294279)
|
|---|
| 研究期間 (年度) |
2006 – 2007
|
| 研究課題ステータス |
完了 (2007年度)
|
| 配分額 *注記 |
3,880千円 (直接経費: 3,400千円、間接経費: 480千円)
2007年度: 2,080千円 (直接経費: 1,600千円、間接経費: 480千円)
2006年度: 1,800千円 (直接経費: 1,800千円)
|
|---|
| キーワード | 形式的検証 / モデル検査 / 静的解析 / 形式言語 / アクセス制御 / セキュリティ / 実行履歴 / XML / ソフトウェア学 |
|---|
| 研究概要 |
(1)再帰的プログラムのモデル検査法:実行履歴に基づくアクセス制御付きプログラム(HBACプログラム)の安全性検証法において、種々の最適化を行うことにより、高速検証が行えることを実証した。提案手法ではモデル検査問題を文脈自由文法(CFG)の空判定問題に帰着しており、アクセス権の個数に対して指数的な検証時間を要する。そこでCFGを構成する際、uselessな規則の構成を防ぐ最適化法を提案した。Chinese-Wallポリシとオンラインバンキングシステムの2つの例題について最適化の効果を実測した結果、最適化を行うことにより、前者の例ではアクセス権の数が80個のとき約64秒、後者の例では60個のとき約0.01秒で検証を行えた。
(2)再帰的プログラムの情報フロー解析法:HBACプログラムに対しモデル検査に基づく新しい情報フロー解析法を提案した。これにより、実行系列上に拡張された情報フローに関する性質を調べることができる。また、自己合成法と呼ばれる新しい情報フロー解析法を一般の再帰プログラムに適用できるように拡張した。
(3)実行履歴に基づくアクセス制御モデルの表現能力の比較:セキュリティオートマトン、狭履歴オートマトン、スタック検査、HBACをアクセス制御機構にもつプログラムの表現能力を比較した。
(4)実行履歴に基づくアスペクト折込み機能の形式モデル:pointcut and adviceの形式モデルA-LTSを提案し、A-LTSの受理言語、決定性文脈自由言語、線形文脈自由言語のクラスはすべて互いに他を含まないことを証明した。
(5)その他
(a)等式系と書換え系を内部にもつ木オートマトンの諸性質を明らかにしした。
(b)公開木戦略(DTS)とよばれる信用交渉戦略の計算量および効率の良いDTS実行アルゴリズムを示した。
(c)CFGの構文解析法を応用し、相互作用をもつRNAの2次構造予測法を提案した。
|
