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

2002 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

アクセス制御におけるポリシーとは,「誰が,どのデータに対して,どのような操作を行なうことを許可/禁止するか,または義務であるか」を記述したものをいう.例えば「ユーザはプロバイダからサービスを受けたら対価を支払わなければならない」は義務ポリシーの例である.近年Ponderをはじめ,ポリシー記述言語が種々提案されている.本研究ではまず,以下の特長をもつポリシー記述言語を提案した.
・各オブジェクトが固有のポリシーをもち,オブジェクト間のメッセージ送受信(メソッド呼出し)において,関与するオブジェクトのポリシーに応じて実行が制御される.
・ポリシー記述の形式的意味が定義されており,これに基づき信頼性の高い実装ならびに,安全性の検証法を導くことができる.
ポリシー記述を伴うプログラムを,ポリシー制御システム(Policy Controled System, PCS)と呼ぶ.「PCSPと,LTL式などで記述された検証条件ψが与えられたとき,Pがψを満たすか」を判定する問題を,PCSに対する検証問題と呼ぶ.本研究では,PCSに対する以下のような検証法を提案した:プッシュダウンシステム(PDS)と呼ばれる無限状態系に対して,LTL式の検証問題が決定可能であることが知られている.PCSPと検証条件ψが与えられたとき,次の条件を満たすPDSP^#と検証条件ψ^#に抽象化する.「P^#がψ^#を満たすならば,Pもψを満たす.」さらに,検証条件を安全性AGφ「Pにおいて到達可能なすべての状態がφを満たす」に限った場合について,PDSに対する自動検証を行なう検証系を実装した.実験結果により,比較的複雑な義務ポリシーを伴う場合でも,500ステートメント程度のプログラムに対して数分で安全性の検証が行なえることを実証した.

Research Products

• [Publications] Kuninobu, Takata, Taguchi, Nakae, Seki: "A Specification Languge for Distributed Policy Control"電子情報通信学会技術研究報告. SS2002-19. 25-30 (2002)
• [Publications] Kuninobu, Takata, Taguchi, Nakae, Seki: "A Specification Languge for Distributed Policy Control"4th Int'l. Conf. on Information and Communications Security. LNCS2513. 386-398 (2002)
• [Publications] 新田, 関: "プッシュダウンシステムの拡張およびそのモデル検査法"情報処理学会第42回プログラミング研究会. (印刷中). (2003)
• [Publications] Kuninobu, Takata, Nitta, Seki: "A Verificaton Method for Distributed Policy Control"電子情報通信学会技術研究報告. SS2002-44. 43-48 (2003)
• [Publications] Seki, Nitta, Tanaka, Kuninobu: "Infinite State Model Checking and Its Application to Software Verification"第2回クリティカル・ソフトウェアワークショップ. (印刷中). (2003)