2005 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 |
(1)実行履歴に基づくアクセス制御系の検証法:昨年度我々が提案した実行履歴に基づくアクセス制御系のモデルHBAC(History-Based Access Control)に対し,本年度は検証器の実装を行った.検証器は,与えられたHBACプログラムの実行系列を生成する文脈自由文法(CFG)Gを構成し,Gの生成する言語L(G)が検証性質を表す正則言語L(R)に包含されるかどうかを判定する.単純な実装ではGのサイズがアクセス権の種類に対して指数的となり実用的でない.そこで,(a)Gの開始記号から生成規則によって到達可能な非終端記号のみを幅優先探索で構成する,(b)Gの各非終端記号Aには,Aの表す実行区間の先頭と末尾においてプログラムのもつアクセス権集合が埋め込まれているが,実行区間末尾におけるアクセス権集合を先行計算(部分計算)することにより,構成すべき非終端記号の個数を減らす,という2種の最適化を実装した.これにより,オンラインバンキングシステムをモデル化したHBACプログラムにおいて,アクセス権の総数が24のとき,最適化(a)のみでは検証に約71秒要したのに対して,(a)(b)を共に行うことにより0.24秒に短縮できた.
(2)XMLアクセス制御における静的解析法:昨年度に引き続き,XMLデータベースにおける要素レベルアクセス制御について木オートマトン理論を用いて考察した.本年度は我々の問合せモデルがNevenのquery automatonより真に表現能力が大きいことを示した.また,スキーマ変換Φとその入力/出力スキーマにおけるアクセス制御ポリシーPin.Poutが与えられたとき,「Pinによって保護されるデータは,Φによる変換後もPoutによって保護されること」を検証する問題が判定可能であることを示した.
(3)内部状態を考慮した信用管理システム:PKI(公開鍵基盤)ディジタル証明書の認証に基づく信用管理システムにおいて,システムの内部状態を考慮した形式モデルならびにそのモデル検査法を提案した.さらに,モデル検査器SPINとPrologを組み合わせた検証法とPrologのみを用いた検証法を実装し,後者の方が検証効率が良いことを実証した.
|
Research Products
(6 results)
