| 研究概要 |
セキュアプロトコル/システム(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電子支払プロトコルがいくつかの望ましい性質を有すことの検証を行った.
|
