研究課題
基盤研究(C)
2年間の研究期間内に以下に挙げる成果を得た。これにより、ソフトウェアコンポーネントの整合性検査とそれにもとつく実行時安全性の検査手法に関する新たな知見を得ることができた。(a)スケーラブルな仕様記述とそれにもとづくコンポーネントの整合性検査手法研究代表者と研究分担者はアスペクト指向仕様記述言語Moxaの設計開発を行った。実際のソフトウェアモジュールの仕様記述実験を行い、モジュールあたりの仕様記述量およびコードの変更に伴う仕様記述への修正箇所を大幅に抑えられることを示した。また一般に、状態遷移に関する制約条件などのプログラムの抽象的な振る舞いに関する性質を仕様記述から抽出することは、仕様記述をスケーラブルにする上で効果的である。しかし従来の表明記述方式ではそのような動作が把握しづらく、検証の際にも付帯条件が必要となり扱いづらい。研究代表者は、Moxaの表明アスペクトを利用してコンポーネントの状態遷移を直接記述できるような拡張記述方式を提案した。本拡張記述方式により、複数コンポーネントに横断する状態遷移に関する記述が可能になり、状態遷移記述の合成が容易になることを示した。(b)実行時検査にもとづく安全性検査手法研究代表者は、隠れチャネル(covert channel)と呼ばれる、本来は情報を伝えることを想定していない手段を介した情報漏洩の一種を、実行監視によって検知可能であることを明らかにした。この研究はSchneiderらによる実行監視に関する理論的研究をベースとしたもので、拡張モニタと呼ばれる機構を用いることで情報流に関するポリシーが強制可能であることを示したものである。監視される対象の動作を模倣する構造を内包するモニタ(拡張モニタ)を用いることで、情報流に関する性質の一つである非推論性(noninference)を含んだ、より広い性質を規定するポリシーが強制可能であることを明らかにした。
すべて 2006 2005
すべて 雑誌論文 (10件)
IEEE Int1. Symp. on Frontiers of Availability, Reliability and Security (FARES)
ページ: 577-584
Electronic Notes in Theoretical Computer Science 163・1
ページ: 45-56
International Symposium on Frontiers in Availability, Reilability and Security (FARES)(IEEE Press)
Electronic Notes in Theoretical Computer Science(Elsevier) 163 (1)
情報処理学会論文誌(プログラミング) 46・SIG11
ページ: 27-44
Workshop on Dependable Software : Tools and Methods (Suppl. Vol. IEEE DSN 2005)
ページ: 221-227
ECOOP 2005 Workshop on Reflection, AOP and Meta-Dat a for Software Evolution (RAM-SE'05)
ページ: 29-38
IPSJ Journal (PRO) Vol.46, No.SIG 11 (PRO 26)
Workshop on Dependable Software-Tools and Methods (Supplemental Volume of the 2005 International Conference on Dependable Systems and Networks (DSN 2005))(IEEE Press)
2nd ECOOP 2005 Workshop on Reflection, AOP and Meta-Data for Software Evolution (RAM-SE '05)
