2002 Fiscal Year Annual Research Report
| Project/Area Number |
12133206
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
二木 厚吉 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (50251971)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
天野 憲樹 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (30313703)
森 彰 産業技術総合研究所, 研究員 (30311682)
岡田 光弘 慶應義塾大学, 文学部, 教授 (30224025)
|
|---|
| Keywords | システム安全性 / 形式手法 / CafeOBJ / 検証 / ウィルス検査 / 電子商取引プロトコル / 認証プロトコル |
|---|
| Research Abstract |
システムの要求や仕様を振舞や観測(behavior or observation)レベルで定式化/記述できる振舞仕様(behavioral specification)を採用し,それに基づきシステムの安全性の検証を,適切な抽象度のモデルやアルゴリズムに基づき,厳密かつ十分に数学的に行う技術の開発を目的として,以下の研究を行った.
(1)線形論理に基づく実時間システムとセキュリティプロトコルの安全性検証:線形論理を用いて実時間システムの安全性検証のための論理学的方法論を構築することを目的とし,特にエージェントの数の増加や時間制約が動的に変化するシステムの分析にも我々の論理的方法論が適用可能であることを明らかにした.又,本枠組を時刻認証子付のセキュリティプロトコルの分析に応用した.またこの過程で安全性評価のためのBAN推論を整理し簡潔にした.
(2)新しいウィルス防御法:x86プロセッサー上でのWin32実行ファイル形式のコンピューターウィルスを,パターン定義に依存することなく未知の状態で検知する新しい技術を研究開発した.具体的には,コードシミュレーションによる暗号復号とコード静的解析によるAPI関数呼び出しレベルでの振る舞い解析を行うことにより,ファイル感染や無差別メール送出といったウィルス特有の振る舞いを検知するものである.禁止すべき振る舞いをポリシーとして別途定義しておくことにより,様々な振る舞いを検知することが可能になる新たなウィルス防御法を開発した.作成したツールを用いたポリシー検査実験により,Aliz, MyParty, Badtrans, Klezといった実際に蔓延したウィルスを,その振る舞いを静的に検査することにより未知状態で検知することが可能であることを確認することができた.
(3)振舞仕様に基づく電子支払プロトコルの検証:iKP電子支払プロトコルおよびHorn-Preneel少額支払プロトコルがある重要と思われる性質を有することを検証した.具体的には,(1)プロトコルを振舞遷移機械としてモデル化する,(2)モデルをCafeOBJで記述する,(3)検証したい性質をCafeOBJの項で表現する,(4)その性質をプロトコルが有することを示す証明譜をCafeOBJで記述する,(5)CafeOBJシステムで証明譜を実行することで証明の正しさを確認する,という手続きでCafeOBJ言語とその処理系を用いて検証した.
|
-
[Publications] Kokichi, Futatsugi: "Formal Methods in CafeOBJ"Lecture Notes in Computer Science. 2441. 1-20 (2002)
-
[Publications] R.Diaconescu, K.Futatsugi: "Logical Foundations of CafeOBJ"Theoretical Computer Science. 281. 471-198 (2002)
-
[Publications] Mitsuhiro Okada: "A Uniform Semantic Proof for Cut-Elimination and Completeness of Various First and Higher Order Logics"Theoretical Computer Science. 172-179 (2000)
-
[Publications] K.Ogata, K.Futatsugi: "Rewriting-Based Verification of Authentication Protocols"4th International Workshop on Rewriting Logic and its Applications, ENTCS. 71. (2002)
-
[Publications] A.Mori, K.Futatsugi: "CafeOBJ as a Tool for Behavioral System Verification"International Symposium on Software Security, LNCS. 2609(To appear). (2003)
-
[Publications] K.Ogata, K.Futatsugi: "Formal Analysis of the iKP Electronic Payment Protocols"International Symposium on Software Security, LNCS. 2609(To appear). (2003)
