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

2002 年度 実績報告書

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

研究概要

誤りの無いシステムの構築と人為的な攻撃に対して耐性のある、安全なシステムの構築を、形式手法によりサポートするための理論と技術について、以下の成果を得た。
まず、DoS攻撃耐性に関する解析のための形式的計算体系としてPi計算を拡張したSpice計算に、型概念を導入しコスト浪費に関する推論を可能とした。また、プログラム変換を行いコスト監視のコード断片を挿入することにより、安全性を向上する手法を提唱し、そのプロトタイプシステムを実装した。
さらに時間論理によるリアクティブシステム仕様の実現可能性に関わる検証について、実装時における様々な効率化手法を提案し、さらに高級言語による仕様記述支授や、検証の副産物であるタブローのグラフィカルな表示による、仕様の不備と思われる部分の発見支援など、統合的なユーザインタフェースを持つ検証機を実装した。また、UMLステートチャートが、未定義の動作や矛盾を含まないか等を検証する手法を示した。
リレーサーバを用いたPOP before SMTPの実現について研究を行なった。これは、POPのリレーサーバとSMTPサーバとの組み合わせにより、メールスプールの保護と、POPサーバの拡張を行わないPOP before SMTPを可能とすると同時に、クライアントの間のPOPセッションは、リレーサーバによりSSL上で実行する方式を与え実装した。
またプロトコル検証については、Spi計算の型付けによる公開鍵暗号方式を用いたプロトコルにおけるメッセージ認証の検証方式について検討を行った。また、否認不可避署名方式を用いた入札プロトコルが持つべき様々な性質を形式化し、これまで行われてきた認証プロトコルの検証方式を拡張した。
一方安全なハードウェアの検証と合成の研究として、非同期式システムの検証に関してより直感的で同期式回路設計者にも理解しやすいレベル指向非同期式回路モデルを提案し、その解析を高速に行うpartial order reduction技術を用いた検証手法を開発した。

研究成果

• [文献書誌] 青島武伸, 米崎直樹: "時間論理によるリアクティブシステム仕様の検証の効率化"コンピュータソフトウェア. 5月号. (2003)
• [文献書誌] Takenobu Aoshima, Takahiro Ando, Naoki Yonezaki: "Consistency Checking of Behavioural Modeling in UML Statechart Diagrams"European Japanese Conference on Information modelling and Knowledge. 179-196 (2002)
• [文献書誌] 増井健司, 友石正彦, 米崎直樹: "SSLとリレーサーバを用いたPOP before SMTPのセキュアな実現法"電子情報通信学会誌. 4月号. (2003)
• [文献書誌] T.Yoneda, T.Kitai, C.Myers: "Automatic Derivation of Timing Constraints by Failure Analysis"Proc. of Computer Aided Verification. 195-208 (2002)
• [文献書誌] B.Zhou, T.Yoneda, C.Myers: "Framework of Timed Trace Theoretic Verification Revisited"電子情報通信学会英文論文誌. Vol.E85-D, No.10. 1595-1604 (2002)
• [文献書誌] T.Yoneda, E.Mercer, C.Myers: "Modular Synthesis of Timed Circuits using Partial Order Reduction"電子情報通信学会英文論文誌. Vol.E85-A, No.12. 2684-2692 (2002)
• [文献書誌] Noriaki Yoshiura: "Logic of Relevant Connectives for Knowledge Base Reasoning"Information modeling and knowledge bases XIV, IOS Press. (2002)