2004 Fiscal Year Annual Research Report
| Project/Area Number |
16500019
|
|---|
| Research Institution | Nara Institute of Science and Technology |
|---|
Principal Investigator |
関 浩之 奈良先端科学技術大学院大学, 情報科学研究科, 教授 (80196948)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
高田 喜朗 奈良先端科学技術大学院大学, 情報科学研究科, 助手 (60294279)
|
|---|
| Keywords | 形式的検証 / モデル検査 / アクティブソフトウェア / アクセス制御 / 静的解析 / 実行履歴 / 形式言語 / セキュリティポリシー |
|---|
| Research Abstract |
本年度は,主に以下の2つの研究成果を得た.
(1)実行履歴に基づくアクセス制御系の形式モデルとその検証法:現在,Java言語等の実行時環境では,スタック検査と呼ばれる動的アクセス制御法が広く用いられている.しかし,スタック検査は実行が完全に終了したメソッドに関する情報をアクセス制御に用いることができないという問題点をもつ。これを解決するため,AbadiとFournetは2003年に実行履歴に基づくアクセス制御法を提案し,C^#実行時環境上で実装を行った.しかしAbadiらの制御法には形式モデルがなく,アクセス制御が所望のセキュリティゴールを満たしているかどうかの厳密な議論はできなかった.
そこで本研究ではまず,Abadiらのアクセス制御法を包摂するHBAC(History-Based Access Control)プログラムという形式モデルを提案した.HBACプログラムでは各メソッドに静的アクセス権が割り当てられる.プログラム実行時にはプログラムのもつ実効アクセス権(集合)がメソッド呼出しとそこからの復帰ごとに変化していく.動的アクセス制御はcheck文とよばれる制御文の実行によって行われる.check文が実行されると,そのcheck文のパラメータとして指定されたアクセス権すべてが,その時点でのプログラムの実効アクセス権となっているかどうかが検査され,もしそうでなければ実行がアボートされる.このcheck文の機能がアクティブソフトウェアの典型例となっている.以上のHBACモデルに対して,トレース集合の安全性検証問題を定義し,この検証問題が一般には決定性指数時間完全であること,アクセス権の種類がプログラム長の対数オーダ以下であれば多項式時間可解であることを示した.
(2)XMLアクセス制御における静的解析法:XMLデータベースにおける要素レベルアクセス制御について,データベースへの問合せがアクセス制御ポリシーに違反しないかどうかを静的に解析する手法を,木オートマトン理論を用いて判定するアルゴリズムを提案した.
|
