動的アクセス制御を行なうソフトウェアのセキュリティ検証に関する研究

2003 Fiscal Year Annual Research Report

• Project/Area Number: 14580376
• Research Institution: NARA INSTITUTE OF SCIENCE AND TECHNOLOGY
• Principal Investigator: 関 浩之 奈良先端科学技術大学院大学, 情報科学研究科, 教授 (80196948)
• Co-Investigator(Kenkyū-buntansha): 新田 直也 奈良先端科学技術大学院大学, 情報科学研究科, 助手 (20346307) ; 高田 喜朗 奈良先端科学技術大学院大学, 情報科学研究科, 助手 (60294279)
• Keywords: アクセス制御 / セキュリティ / 安全性 / 検証 / モデル検査 / ポリシー

Research Abstract

動的アクセス制御を行うソフトウェアに固有の自動検証法について、昨年度に引き続き以下の研究を行った。
(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(公開鍵基盤)に基づく信用管理システムの新しいモデルを提案した。

Research Products

• [Publications] Hitoshi Ohsaki, Hiroyuki Seki, Toshinori Takai: "Recognizing Boolean Closed A-Tree Languages with Membership Conditional Rewriting Mechanism"14^<th> Int'l Conference on Rewriting Techniques and Applications. LNCS2706. 483-498 (2003)
• [Publications] Naoya Nitta, Hiroyuki Seki: "An Extension of Pushdown System and Its Model Checking Method"14^<th> Int'l Conference on Concurrency Theory. LNCS2761. 281-295 (2003)
• [Publications] 八木勲, 高田喜朗, 関浩之: "ラベル付き遷移システムに基づくアスペクト指向プログラムのモデル化"電子情報通信学会技術研究報告. SS2003-46. 1-6 (2004)
• [Publications] 毛利寿志, 高田喜朗, 関浩之: "システムの内部状態を導入した信用管理モデル"電子情報通信学会2004年総合大会講演論文集. A-7-2 (2004)
• [Publications] 高田喜朗, 関浩之: "アスペクト指向プログラミングのための状態遷移型モデル"第3回クリティカルソフトウェアワークショップ予稿集. (発表予定). (2004)