| 研究分担者 |
飯田 周作 専修大学, ネットワーク情報学部, 専任講師 (80338590)
緒方 和博 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (30272991)
森 彰 産業技術総合研究所, サイバーアシストセンター, グループリーダー (30311682)
中村 正樹 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (40345658)
天野 憲樹 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (30313703)
岡田 光弘 慶應義塾大学, 文学部, 教授 (30224025)
|
|---|
| 配分額 *注記 |
30,800千円 (直接経費: 30,800千円)
2003年度: 5,800千円 (直接経費: 5,800千円)
2002年度: 10,700千円 (直接経費: 10,700千円)
2001年度: 14,300千円 (直接経費: 14,300千円)
|
|---|
| 研究概要 |
一貫した論理体系に基づき,適応性と汎用性に優れ,かつ自動化の容易な安全性検証技術を実現することを目標に研究を進め,振舞仕様に基づく以下のような技術を開発した.
(1)未知ウイルス検知技術:振舞仕様の理論的枠組に基いてプログラムの挙動をモデル化することで,プログラムの安全性(=ウイルスで「あること」ならびに「ないこと」の判定)を論理的に解析し,自動的に検知する枠組を提案し,処理系を作成した.具体的には,Microsoft社のWindows OS上のプログラムを対象として,未知ウィルス検知ソフトウェアを作成し,開発した技術の有効性を示した.
(2)振舞仕様に基づく安全性検証技術:システムの安全性(safety)を,よりユーザーやアプリケーションに近いレベルで検証する技術として,システムの要求や仕様を振舞(behavior)レベルで定式化し,それに基づきシステムの安全性をよりユーザに近いレベルで検証し得る技術を研究開発し,それを鉄道信号システム,コンポーネントウェア,並行分散システム,安全プロトコルなどに適用し,その有効性を示した.特に電子商取引プロトコルに付いては,実規模のプロトコルの検証を行った.
(3)振舞仕様に基づくモデル検査技術:システムの要求や仕様を振舞(behavior)レベルで定式化し,システムの状態を仕様レベルで自然に抽象化することで,一般には無限状態となるシステムに対しても有効なモデル検査技術を開発し,基本的な並行アルゴリズムにや通信プロトコルについてこの技術の有効性を示した.
|
