研究課題
最終年度である本年度は、以下の成果を得た。これにより、ソフトウェアコンポーネントの整合性検査とそれにもとづく実行時安全性の検査手法に関する一定の成果を得ることができた。(a)スケーラブルな仕様記述とそれにもとづくコンポーネントの整合性検査手法本年度は、前年度より設計開発を行っていた仕様記述言語Moxaを拡張し、その効果を明らかにした。一般に、仕様記述から(コンポーネントの状態遷移に関する制約条件などの)プログラムの抽象的な振る舞いに関する性質を抽出することは、仕様記述をスケーラブルにする上で効果的である。しかし従来の論理式による(フラットな)表明記述ではそのような動作が把握しづらく、検証の際にも付帯条件が必要となり扱いづらい。研究代表者は、Moxaの表明アスペクトを利用して、コンポーネントの状態遷移を直接記述できるような拡張記述方式(プロトコル記述)を提案した。この拡張記述方式は、(1)複数コンポーネントに横断する状態遷移に関する記述が可能にし、(2)状態遷移記述の合成を容易にする。(b)実行時検査にもとづく安全性検査手法研究代表者は、隠れチャネル(covert channel)と呼ばれる、本来は情報を伝えることを想定していない手段を介した情報漏洩の一種を、実行監視によって検知可能であることを明らかにした。この研究はSchneiderらによる実行監視に関する理論的研究をベースとしたもので、拡張モニタと呼ばれる機構を用いることで情報流に関するポリシーが強制可能であることを示したものである。監視される対象の動作を模倣する構造(エミュレータ)を内包するモニタ(拡張モニタ)を用いることで、情報流に関する性質の一つである非推論性(noninference)を含んだ、より広い性質を規定するポリシーが強制可能であることを明らかにしている。
すべて 2006
すべて 雑誌論文 (4件)
Electronic Notes in Theoretical Computer Science 163・1
ページ: 45-56
International Symposium on Frontiers in Availability, Reilability and Security (FARES)
ページ: 577-584
情報処理学会研究報告(コンピュータセキュリティ研究会) 2006-CSEC-34
ページ: 207-214
情報処理学会研究報告(ソフトウェアエ学研究会) 2006-SE-153
ページ: 15-22
