| 研究課題/領域番号 |
17500017
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
ソフトウエア
|
|---|
| 研究機関 | 東京工業大学 |
|---|
研究代表者 |
渡部 卓雄 東京工業大学, 大学院・情報理工学研究科, 助教授 (20222408)
|
|---|
| 研究分担者 |
山田 聖 産業技術総合研究所, 情報セキュリティ研究センター, 研究員 (80415760)
|
|---|
| 研究期間 (年度) |
2005 – 2006
|
| 研究課題ステータス |
完了 (2006年度)
|
| 配分額 *注記 |
3,200千円 (直接経費: 3,200千円)
2006年度: 1,500千円 (直接経費: 1,500千円)
2005年度: 1,700千円 (直接経費: 1,700千円)
|
|---|
| キーワード | 形式仕様記述 / 契約による設計 / アスペクト指向 / モデル駆動開発 / 実行時検査 / 隠れチャネル / 情報漏洩 / 状態遷移記述 / オントロジー |
|---|
| 研究概要 |
2年間の研究期間内に以下に挙げる成果を得た。これにより、ソフトウェアコンポーネントの整合性検査とそれにもとつく実行時安全性の検査手法に関する新たな知見を得ることができた。
(a)スケーラブルな仕様記述とそれにもとづくコンポーネントの整合性検査手法
研究代表者と研究分担者はアスペクト指向仕様記述言語Moxaの設計開発を行った。実際のソフトウェアモジュールの仕様記述実験を行い、モジュールあたりの仕様記述量およびコードの変更に伴う仕様記述への修正箇所を大幅に抑えられることを示した。また一般に、状態遷移に関する制約条件などのプログラムの抽象的な振る舞いに関する性質を仕様記述から抽出することは、仕様記述をスケーラブルにする上で効果的である。しかし従来の表明記述方式ではそのような動作が把握しづらく、検証の際にも付帯条件が必要となり扱いづらい。研究代表者は、Moxaの表明アスペクトを利用してコンポーネントの状態遷移を直接記述できるような拡張記述方式を提案した。本拡張記述方式により、複数コンポーネントに横断する状態遷移に関する記述が可能になり、状態遷移記述の合成が容易になることを示した。
(b)実行時検査にもとづく安全性検査手法
研究代表者は、隠れチャネル(covert channel)と呼ばれる、本来は情報を伝えることを想定していない手段を介した情報漏洩の一種を、実行監視によって検知可能であることを明らかにした。この研究はSchneiderらによる実行監視に関する理論的研究をベースとしたもので、拡張モニタと呼ばれる機構を用いることで情報流に関するポリシーが強制可能であることを示したものである。監視される対象の動作を模倣する構造を内包するモニタ(拡張モニタ)を用いることで、情報流に関する性質の一つである非推論性(noninference)を含んだ、より広い性質を規定するポリシーが強制可能であることを明らかにした。
|
