論理的仕様を基礎としたセキュアシステムの検証法

2003 年度 実績報告書

• 研究課題/領域番号: 12133204
• 研究機関: 東京工業大学
• 研究代表者: 米崎 直樹 東京工業大学, 大学院・情報理工学研究科, 教授 (00126286)
• 研究分担者: 吉浦 紀晃 群馬大学, 総合情報処理センター, 助教授 (00302969) ; 西崎 真也 東京工業大学, 大学院・情報理工学研究科, 助教授 (90263615) ; 米田 友洋 国立情報学研究所, 情報基盤研究系, 教授 (30182851) ; 友石 正彦 東京工業大学, 大学院・情報理工学研究科, 助手 (60262284)
• キーワード: 安全性検証 / 暗号方式 / セキュリティプロトコル / ネットワークセキュリティ / Dos攻撃 / 非同期回路 / 仕様解析 / コード生成

研究概要

以下の項目について研究を行った。
セキュリティプロトコルの検証・合成、暗号方式の検証 (1)理想的な非対称暗号方式において攻撃者が獲得可能な情報を推論する体系を提案し、暗号方式の多くの安全性をこの体系の演繹に関する性質として形式化し証明した。(2)セキュリティプロトコル自動設計アルゴリズムを与えた。構造要件を満たすかどうかのみを調べることで、より少ない計算コストでの自動生成が可能となった。(3)DoS攻撃に対するプロトコルの耐性に関する解析を行うための形式的枠組みとして、計算体系Spice計算を提唱し、これまで知られているDoS攻撃を解析した。(4)ネットワークオークションでの入札者の公平性検証に必要な形式化を行い検証した。
ネットワークシステムの安全性検証・実装 (1)従来、プログラムの基礎付けや解析に用いられてきた数学的モデルを拡張し、ネットワークプロトコルにおけるサービス拒否攻撃やWWWに対するクライアントサイドスクリプトを用いたブラウザ破壊攻撃などの現象の解析に応用した。(2)リレーサーバを用いてPOP before SMTPを実現する方法について研究を行なった。この実装により、POP serverの更新管理とそのネットワーク利用における安全管理を切り離すことが可能となった。
ハードウェアの検証と合成 昨年度開発したタイミング制約の自動導出アルゴリズム、および、高速timing failure検出アルゴリズムについて、正当性を証明した。一方ハードウェア記述言語SpecCの抽象レベル記述を入力とし、演算器数の制約のもと、資源のスケジューリング、および、レジスタ割当を行った上で、ゲートレベル非同期式回路を自動生成する高位合成システムの開発を行った。
リアクティブシステム仕様の検証・合成・実装 (1)時間論理によるりアクティブシステム仕様がプログラム化可能であるための必要条件のいくつかについて、仕様がそれらの条件を満たさないことの原因を形式的に定義し、その導出手続きを、仕様の充足可能性判定手続きであるタブロー法を拡張することで構成した。(2)状態爆発を押えるために代表状態の導入、BDDなどによるsymbolic手法の導入に加え、新たに構築した分割検証方法を導入した検証器の実装を行い、他の代表的な検証器との比較実験において良好な結果を得た。
安全な最適コードの自動生成 コンパイラでは様々なコード最適化手法が導入され複雑になった結果、生成コードの安全性が自明ではない。ここでは、コンパイラにおいて自動的に誤りがないコード最適化を行う新しい方式として、時間論理におけるモデル生成の手法を提案した。

研究成果

• [文献書誌] 蜷川忠三, 青井文男, 横浜浩二, 米田友洋: "空調制御ネットワークにおける信号極性確定の分散アルゴリズム"電気学会論文誌C. 123巻5号. 919-927 (2003)
• [文献書誌] Tomoya Kitai, Yusuke Oguro, Tomohiro Yoneda, Eric Mercer, Chris Myers: "Partial Order Reduction for Timed Circuit Verification of Based on a Level Oriented Model"電子情報通信学会英文論文誌. Vol.E86-D No.12. 2601-2611 (2003)
• [文献書誌] Takenobu Aoshima, Takahiro Ando, Naoki Yonezaki: "Consistency Checking of Behavioural Modeling in UML Statechart Diagrams"Information Modeling and Knowledge bases XIV(IOS Press). 152-169 (2003)
• [文献書誌] 青島武伸, 米崎直樹: "時間論理によるリアクティブシステム仕様の検証の効率化"コンピュータソフトウェア. Vol.20 No.3. 30-53 (2003)
• [文献書誌] Shin-ya Nishizaki, Naoki Uesugi: "Secure Filtering of Client-Side Scripts by Program Transformation"Information Technology Letters. 37-39 (2003)
• [文献書誌] Noriaki Yoshiura: "Logic of Relevant Connectives for Knowledge Base Reasoning"Information Modeling and Knowledge bases XIV(IOS Press). 66-80 (2003)
• [文献書誌] 増井健司, 友石正彦, 米崎直樹: "SSLとリレーサーバを用いたPOP before SMTPのセキュアな実現法"電子情報通信学会誌. Vol.J86-DJ No.4. 260-268 (2003)
• [文献書誌] 米田友洋(訳): "非同期式回路の設計(C.Myers : Asynchronous Circuit Design)"共立出版. 416 (2003)