2006 Fiscal Year Annual Research Report
静的解析と実行時検査の融合にもとづくソフトウェアの安全な動的構成と実行方式
| Project/Area Number |
17500017
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
渡部 卓雄 東京工業大学, 大学院・情報理工学研究科, 助教授 (20222408)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
山田 聖 産業技術総合研究所, 情報セキュリティ研究センター, 研究員 (80415760)
|
|---|
| Keywords | 形式仕様記述 / 契約による設計 / アスペクト指向 / モデル駆動開発 / 実行時検査 / 隠れチャネル / 情報漏洩 / 状態遷移記述 |
|---|
| Research Abstract |
最終年度である本年度は、以下の成果を得た。これにより、ソフトウェアコンポーネントの整合性検査とそれにもとづく実行時安全性の検査手法に関する一定の成果を得ることができた。
(a)スケーラブルな仕様記述とそれにもとづくコンポーネントの整合性検査手法
本年度は、前年度より設計開発を行っていた仕様記述言語Moxaを拡張し、その効果を明らかにした。一般に、仕様記述から(コンポーネントの状態遷移に関する制約条件などの)プログラムの抽象的な振る舞いに関する性質を抽出することは、仕様記述をスケーラブルにする上で効果的である。しかし従来の論理式による(フラットな)表明記述ではそのような動作が把握しづらく、検証の際にも付帯条件が必要となり扱いづらい。研究代表者は、Moxaの表明アスペクトを利用して、コンポーネントの状態遷移を直接記述できるような拡張記述方式(プロトコル記述)を提案した。この拡張記述方式は、(1)複数コンポーネントに横断する状態遷移に関する記述が可能にし、(2)状態遷移記述の合成を容易にする。
(b)実行時検査にもとづく安全性検査手法
研究代表者は、隠れチャネル(covert channel)と呼ばれる、本来は情報を伝えることを想定していない手段を介した情報漏洩の一種を、実行監視によって検知可能であることを明らかにした。この研究はSchneiderらによる実行監視に関する理論的研究をベースとしたもので、拡張モニタと呼ばれる機構を用いることで情報流に関するポリシーが強制可能であることを示したものである。監視される対象の動作を模倣する構造(エミュレータ)を内包するモニタ(拡張モニタ)を用いることで、情報流に関する性質の一つである非推論性(noninference)を含んだ、より広い性質を規定するポリシーが強制可能であることを明らかにしている。
|
Research Products
(4 results)
