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