適応的ソフトウェア構築のための宣言的ポリシー記述とその整合性検査方式の研究

2003 Fiscal Year Annual Research Report

• Project/Area Number: 15500028
• Research Institution: National Institute of Informatics
• Principal Investigator: 渡部 卓雄 国立情報学研究所, ソフトウェア研究系, 助教授 (20222408)
• Co-Investigator(Kenkyū-buntansha): 鈴木 正人 国立情報学研究所, 情報学基礎研究系, 助教授 (30242572)
• Keywords: ポリシー強制 / バイトコード変換 / プロセス代数 / 自己検査コード / 実行時検査 / 適応的ソフトウェア / Java / Common-Lisp

Research Abstract

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

Research Products

• [Publications] 一杉裕志(他2名): "安全に結合可能なmixinを提供するためのルール"コンピュータソフトウェア. 20巻3号. 80-87 (2003)
• [Publications] Takuo Watanabe(他2名): "Towards a Specification Scheme for Context-Aware Security Policies for Networked Appliances"IEEE International Workshop on software Technologies for Future Embedded Systems. 65-68 (2003)
• [Publications] Noriki Amano(他1名): "LampJ : A Library of Adaptable Modular Programming for Java"IASTED International conference on Software Engineering and Application. 213-218 (2003)
• [Publications] Takuo Watanabe(他2名): "Specifying Context-Aware Runtime Security Policies using an Algebraic Policy Specification Language"IASTED International Conference on Software Engineering. 612-617 (2004)