| 研究概要 |
動的アクセス制御を行うソフトウェアに固有の自動検証法について、昨年度に引き続き以下の研究を行った。
(1)ポリシー制御系(Policy Controlled System, PCS)の検証法:本研究の中心課題である、PCSに対する安全性検証問題「PCS Pと安全性検証項目ψが与えられたとき、Pの任意の到達可能状態がψを満たすか」のモデル検査法について以下のまとまった成果を得た。本手法では、PCSの検証問題をプッシュダウンシステム(Pushdown System, PDS)の検証問題に帰着して判定する。PDSに対するモデル検査法として知られるEsparzaらのアルゴリズムが時間計算量0(n^3)であるのに対し、提案手法ではこれを0(n)に改善した。昨年度から実装に着手したモデル検査器を改良し、義務ポリシーの因果関係が非常に複雑な1,700行程度のPCSに対しても、数分で自動検証が行えることを実証した。
(2)項書換え系(Term Rewriting System, TRS)の検証法への展開:(1)で述べたPDSはスタック記号系刻上の遷移系といえる。そこで、記号系列を木構造(項)に拡張しTRSを項上の遷移系とみなすことにより、TRSにおける検証問題を定義し次の二つの成果を得た。(a)PDSを自然に拡張したTRSの部分クラスGeneralized Growing TRS(GG-TRS)を導入し、正則保存性を満たすGG-TRSに対して、線形時相論理式のモデル検査が決定可能であることを示した。(b)XMLに代表される構造化文書の形式モデルとして、結合則を満たす関数記号を含むTRS(A-TRS)や木オートマトン(A-TA)が注目されている。本研究ではA-TRSの検証法への第一歩として、A-TAによって受理される木言語のクラスがブール演算について閉じていることを示した。
(3)PCSの義務ポリシーと関連して、アスペクト指向プログラムの状態遷移型モデルを提案した。
(4)アクセス制御技術として注目されているPKI(公開鍵基盤)に基づく信用管理システムの新しいモデルを提案した。
|
