| 研究概要 |
本年度はプロセス代数を基礎とするポリシー記述形式の設計を行い,それによって記述されたポリシーを強制するためのシステム(以下,ポリシー強制系と呼ぶ)を実装した.ポリシー強制系は,ポリシー記述(Pとする)と検査対象となるコード(Tとする)を入力とし,ポリシー強制されたコード(T_P)を出力する.T_Pにはあらかじめポリシー強制系によって自己検査コードが埋めこまれている.T_Pは基本的にはTと同じ動作をするが,ポリシーPに違反する動作は自己検査コードによって検出され,実行時に抑制される.
我々が設計したポリシー記述形式では,検査対象が実行し得る基本操作(例えばシステムコールやライブラリ呼び出しなど)の系列のうち,実行を許可するもののみを代数的に記述する.具体的には,基本操作を抽象化したアクションを原子操作とし,いくつかの操作系列を結合して新たな操作系列を与える演算子を定義している.
実装したポリシー強制系は,入力されたコード中の基本操作のうち,ポリシー記述で検査対象としているものの前後に検査コードを挿入する.検査コードは,有限状態機械を用いてポリシー記述によって許可された実行系列であるか否かを検査する.現時点では,対象はJavaのバイトコードであり,ポリシー強制系はCommom-Lispによって実装されている.
さらに我々のポリシー記述形式では,アクション間のデータ依存関係を明示的に記述することで,無関係の動作を検査対象から除くことができる.これによって,現時点では最大60%程度の無駄な検査コードを省くことができた.
今後は適応に関する具体的なポリシーの記述をこの形式で表すことを検討し,さらにこの形式で記述できるポリシーの理論的な特徴付けを行うことで,整合性検査方式の実現を行う.後者についてはすでに予備的な結果を得ている.
|
