| 研究課題/領域番号 |
14580376
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
計算機科学
|
|---|
| 研究機関 | 奈良先端科学技術大学院大学 |
|---|
研究代表者 |
関 浩之 奈良先端科学技術大学院大学, 情報科学研究科, 教授 (80196948)
|
|---|
| 研究分担者 |
新田 直也 奈良先端科学技術大学院大学, 情報科学研究科, 助手 (20346307)
高田 喜朗 奈良先端科学技術大学院大学, 情報科学研究科, 助手 (60294279)
|
|---|
| 研究期間 (年度) |
2002 – 2003
|
| 研究課題ステータス |
完了 (2003年度)
|
| 配分額 *注記 |
3,200千円 (直接経費: 3,200千円)
2003年度: 1,500千円 (直接経費: 1,500千円)
2002年度: 1,700千円 (直接経費: 1,700千円)
|
|---|
| キーワード | アクセス制御 / セキュリティ / 安全性 / 検証 / モデル検査 / ポリシー |
|---|
| 研究概要 |
アクセス制御におけるポリシーとは,「誰が、どのデータに対して、どのような操作を行なうことを許可/禁止するか、または義務であるか」を記述したものをいう。本研究ではまず、以下の特長をもつポリシー記述言語を設計した。
・各オブジェクトが固有のポリシーをもち、オブジェクト間のメッセージ送受信(メソッド呼出し)において、関与するオブジェクトのポリシーに応じて実行が制御される。
・ポリシー記述の形式的意味が定義されており、信頼性の高い実装ならびに、安全性の検証法を導くことができる。
ポリシー記述を伴うプログラムを、ポリシー制御システム(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ページに対して実験を行った。
|
