2005 Fiscal Year Annual Research Report
静的解析と実行時検査の融合にもとづくソフトウェアの安全な動的構成と実行方式
| Project/Area Number |
17500017
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
渡部 卓雄 東京工業大学, 大学院・情報理工学研究科, 助教授 (20222408)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
山田 聖 産業技術総合研究所, 情報セキュリティ研究センター, 研究員
|
|---|
| Keywords | 形式仕様記述 / 契約による設計 / アスペクト指向 / モデル駆動開発 / 実行時検査 / 隠れチャネル / 情報漏洩 / オントロジー |
|---|
| Research Abstract |
本年度は,研究計画の通りに主に基盤となる個別技術の研究を行い,以下の(a)〜(c)に示す研究成果を得た.これにより,コンポーネントの整合性検査とそれにもとづく実行時安全性の検査手法の研究開発の準備が整ったことになる.
(a)スケーラブルな仕様記述方式とそれにもとづくコンポーネントの整合性検査手法
研究代表者および研究分担者が設計したアスペクト指向仕様記述言語Moxaによる,実行時検査のためのツールの開発を行った.Moxaによって実際のソフトウェアモジュールの仕様記述実験を行い,モジュールあたりの仕様記述量を従来方式(JMLによる仕様記述)の30%程度に抑えることができること,およびコードの変更にともない仕様記述への修正箇所を従来方式の25%程度に抑えられることを示した.さらに,仕様記述を表明アスペクトという単位でモジュール化することにより,モデル駆動開発などでもちいられる手法が適用でき,仕様記述とそれにもとづくコード検証が容易になる可能性を示した.
(b)実行時検査にもとづく安全性検査手法
研究代表者が研究開発を行ってきた実行時検査にもとづく安全性検査手法により,従来の実行時検査では検出が難しかった攻撃について検出できることを示した.具体的には,隠れチャネル(covert channel)と呼ばれる経路による情報漏洩の検出が可能であることを証明した.
(c)コンポーネントの安全な結合方式
D-Parts(Disentangled Parts)と呼ばれるコンポーネント記述方式を提案した.本方式ではオントロジーを用いた記述方式を用いることにより,使用するプログラミング言語から独立し,かつコンポーネントの振る舞いを含めた仕様を記述することができる.
|
