2003 Fiscal Year Annual Research Report
| Project/Area Number |
12133206
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology (JAIST) |
|---|
Principal Investigator |
二木 厚吉 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (50251971)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
中村 正樹 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (40345658)
森 彰 産業技術総合研究所, サイバーアシスト研究センター, グループリーダ (30311682)
|
|---|
| Keywords | システム安全性 / 形式手法 / CafeOBJ / 検証 / ウィルス検査 / 電子商取引プロトコル / 認証プロトコル |
|---|
| Research Abstract |
セキュアプロトコル/システム(secure protocol/system),分散並行システム(distributed concurrent systems),実時間システム(real-time systems)等の,ネットワーク社会において重要な役割を担う基盤ソフトウェアシステムの安全性(safety)を,よりユーザーやアプリケーションに近いレベルで解析・検知・検証する技術を開発することを目標に研究を展開してきた.最終年度である平成15年度は,、未知ウィルス検知システムの開発,振舞仕様に基づく電子支払プロトコルの検証,の2つのテーマについて研究を進め,以下のような成果を得た.
未知ウィルス検知システムの開発:x86プロセッサー上でのWin32実行ファイル形式のコンピューターウィルスを対象として,コードシミュレーションによる暗号復号とコード静的解析によるAPI関数呼び出しレベルでの振る舞い解析を行うことにより,ファイル感染や無差別メール送出といったウィルス特有の振る舞いの検出を行うツールを開発した.これにより,禁止すべき振る舞いをポリシーとして定義しておくことにより,パターン定義に依存することなく未知の状態で,ウィルス特有の有害な振る舞いを検出することが可能であることを示した.
実験の結果,このツールを用いて実際に蔓延したウィルスの大部分を未知状態で検出可能であることを確認できた.これは,サンプルとなるウィルスの解析を通じて有効と考えられるポリシーを定義・実装した後,無害プログラムに対する誤認検査を経て実際の検知実験を行うという作業の繰り返しであったが,その過程で近年のウイルスには共通して用いられる「対アンチウィルスソフト」の仕掛けが多く見られることを解明した。
振舞仕様に基づく電子支払プロトコルの検証:システムの要求や仕様を振舞や観測(behavior or observation)レベルで定式化/記述できる振舞仕様(behavioral specification)を採用し,それに基づきシステムの安全性の検証を,適切な抽象度に基づき,厳密かつ十分に数学的に行う技術を開発してきた.特に,いくつかの事例研究をとおして論理的に分散システムを解析するのに有効なOTS/CafeOBJ法を開発した.
このOTS/CafeOBJ法を用い,NetBill電子商取引プロトコルが商品の原子性を有していないことを発見し,その性質を有するための修正案を考案し,修正版NetBillが商品の原子性を有すことの検証の大部分を行った、また、修正版NetBillがその他のいくつかの望ましい性質を有すことの検証を行った。さらに,SET電子支払プロトコルがいくつかの望ましい性質を有すことの検証を行った.
|
-
[Publications] Kazuhiro OGATA, Kokichi FUTATSUGI: "Flaw and Modification of the iKP Electronic Payment Protocols"Information Processing Letters. 86(2). 57-62 (2003)
-
[Publications] Kazuhiro OGATA, Kokichi FUTATSUGI: "Proof Scores In the OTS/CafeOBJ Method"Springer LNCS (FMOODS 2003, Formal Methods for Open Object-Based Distributed Systems). 2884. 170-184 (2003)
-
[Publications] Razvan DIACONESCU, Kokichi FUTATSUGI, Kazuhiro OGATA: "CafeOBJ : Logical Foundation and Methodologies"Computing and Informatics. 22. 257-283 (2003)
-
[Publications] 緒方和博, 二木厚吉: "書き換えによるセキュリティプロトコルの帰納的検証"コンピュータソフトウェア. 20. 54-72 (2003)
-
[Publications] 清野貴博, 緒方和博, 二木厚吉: "項書換えを用いた安全性検証の組織化"コンピュータソフトウェア. 20. 32-45 (2003)
-
[Publications] Akira MORI: "Detecting Unknown Computer Viruses -- A New Approach"International Symposium on Software Security, LNCS. (To appear).
