| 研究概要 |
アクセス制御におけるポリシーとは,「誰が、どのデータに対して、どのような操作を行なうことを許可/禁止するか、または義務であるか」を記述したものをいう。本研究ではまず、以下の特長をもつポリシー記述言語を設計した。
・各オブジェクトが固有のポリシーをもち、オブジェクト間のメッセージ送受信(メソッド呼出し)において、関与するオブジェクトのポリシーに応じて実行が制御される。
・ポリシー記述の形式的意味が定義されており、信頼性の高い実装ならびに、安全性の検証法を導くことができる。
ポリシー記述を伴うプログラムを、ポリシー制御システム(Policy Controlled System、PCS)と呼ぶ。
(1)PCSの検証法:本研究の中心課題である、安全性検証問題「PCS Pと安全性検証項目ψが与えられたとき、Pの任意の到達可能状態がψを満たすか」のモデル検査法について以下の成果を得た。本手法では、PCSの検証問題をプッシュダウンシステム(Pushdown System, PDS)の検証問題に帰着して判定する。PDSに対するモデル検査法として知られるEsparzaらのアルゴリズムが時間計算量O(n^3)であるのに対し、提案手法ではこれをO(n)に改善した。提案アルゴリズムに基づくモデル検査器を実装し、義務ポリシーの因果関係が非常に複雑な1,700行程度のPCSに対しても、数分で自動検証が行えることを実証した。
(2)項書換え系(TRS)の検証法への展開:PDSを自然に拡張したTRSの部分クラスGeneralized Growing TRS (GG-TRS)を導入し、正則保存性を満たすGG-TRSに対して、線形時相論理式のモデル検査が決定可能であることを示した。
(3)構造化文書解析への応用:XML文書dとアクセシビリティガイドラインSが与えられたとき、dがSを満たすかどうかを自動判定するツールを作成し、米国、日本の主要40サイトの約3,000ページに対して実験を行った。
|
