| 研究概要 |
(1)実行履歴に基づくアクセス制御系の検証法:Abadiらのアクセス制御法を包摂するHBAC(History-Based Access Control)プログラムという形式モデルを提案した.次に,HBACモデルに対して安全性検証問題を定義し,この検証問題が一般には決定性指数時間完全であること,アクセス権の種類がプログラム長の対数オーダ以下であれば多項式時間可解であることを示した.提案手法に基づき実装した検証器は,与えられたHBACプログラムの実行系列を生成する文脈自由文法(CFG)Gを構成し,Gの生成する言語が検証性質を表す正則言語に包含されるかどうかを判定する.検証器では,文法における導出に関与しない生成規則の構成を回避するための(a)(b)2種の最適化を実装した.これにより,オンラインバンキングシステムをモデル化したHBACプログラムにおいて,アクセス権の総数が24のとき,最適化(a)のみでは検証に約71秒要したのに対して,(a)(b)を共に行うことにより0.24秒に短縮できた.
(2)XMLアクセス制御における静的解析法:XMLデータベースへの問合せがアクセス制御ポリシーに違反しないかどうかを静的に解析する手法を,木オートマトン理論を用いて判定するアルゴリズムを提案した.また,我々の問合せモデルがNevenのquery automatonより真に表現能力が大きいことを示した.さらに,スキーマ変換Φとその入力/出力スキーマにおけるアクセス制御ポリシーPin,Poutが与えられたとき,「Pinによって保護されるデータは,Φによる変換後もPoutによって保護されること」を検証する問題が判定可能であることを示した.
(3)内部状態を考慮した信用管理システム:PKI(公開鍵基盤)ディジタル証明書の認証に基づく信用管理システムにおいて,システムの内部状態を考慮した形式モデルならびにそのモデル検査法を提案した.さらに,モデル検査器SPINとPrologを組み合わせた検証法とPrologのみを用いた検証法を実装し,後者の方が検証効率が良いことを実証した.
|
