| 研究概要 |
本研究課題における成果は,(1)プロセス代数にもとづくコンポーネントのポリシー記述形式とその強制系,および(2)アスペクト指向にもとづくスケーラブルなコンポーネント間の整合性検査方式の2つに分類することができる.
(1)ポリシー記述形式とその強制系:初年度はプロセス代数を基礎とするポリシー記述形式の設計を行い,それによって記述されたポリシーを強制するためのシステム(以下,ポリシー強制系と呼ぶ)Taurus-1を実装した.我々はこれをF.Schneiderらによるポリシー強制の定式化手法にもとづいてモデル化してその性質を調べる事で,従来のセキュリティオートマトンでは表現できなかった,ある種の情報流に関するポリシーが表現できることを示した.
(2)スケーラブルなコンポーネントの整合性検査方式:契約による設計(Design by Contract, DbC)は,コンポーネントの外部仕様を表明と呼ばれる論理式の集まりで表現するものであり,コンポーネントの仕様記述と整合性検査に有効とされている.しかしコードの規模が大きくなるにつれて,表明の記述量の増大,および表明間の依存関係の複雑化が問題となる.我々はアスペクト指向の考え方を用いて横断的関心事を含む表明をモジュール化する方式を考案し,それに基づく仕様記述言語Moxaを設計・実装した.従来方式ではコンポーネントあたり数千行にわたるような仕様を,Moxaを用いることでモジュールあたり数十行程度に抑えることができ,かつ変更も容易であることを示した.
|
