| 研究概要 |
XMLデータベースのためのアクセス制御を,木オートマトン理論に基づく静的解析によって効率化する方法の研究を行っている.本研究では,アクセス制御ポリシーおよび問い合わせを,それぞれ木オートマトンでモデル化する.アクセス制御ポリシーは本来,XMLデータベースのインスタンスを表す木が与えられたときに,各頂点にアクセス許可または禁止のラベルを割り当てる規則のことである.ここではこれを,各頂点に+または-をラベル付けした木を受理する木オートマトンとしてモデル化する.問い合わせについては,アクセスする頂点・しない頂点をそれぞれ+および-のラベルで表すことで,同様に木オートマトンでモデル化する.これらのモデル化の下で,問い合わせがアクセス制御ポリシーに違反するかどうか判定する問題は,木オートマトンの言語の包含性判定に帰着される.
本研究では,同じデータベースインスタンスに対して複数の+-割り当てを行うアクセス制御ポリシーが与えられたときの解釈として,AND意味論とOR意味論という二つの意味論を定義した。OR意味論の方がAND意味論より表現能力が高いが,静的解析の計算量は,AND意味論では多項式時間可解であるのに対し,OR意味論では決定性指数時間完全である.また,OR意味論が等価なAND意味論のアクセス制御ポリシーを持つかどうか判定する問題も決定性指数時間完全であることがわかった.
オートマトン理論に基づくアクセス制御機構の解析に関連して, Abdaiらが提案した履歴に基づくアクセス制御機構のモデル化と検証法について研究を行った.そして,モデル検査問題が一般には決定性指数時間完全であることを示し,またモデル検査法の計算量を低減するための最適化法を提案した.さらに,モデル検査法を応用して情報流解析を行う方法を提案した.
|
