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

2001 年度 実績報告書

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

研究概要

正しく作られたシステムであっても、人為的な攻撃によって、システムの意図がねじ曲げられたり正しい動作を阻害されたりする。これらを防御するための方法として、以下の成果を得た。
1.セキュリティプロトコルの検証と合成 これまで、並行セッションの情報を用いた攻撃をも考慮した検証体系について研究を行って来たが、本年度はその成果の中で抽出された安全であるための、メッセージの新しさを保証するランダムなデータであるナンスと暗号化の利用要件を用いると同時に、参加者の知識集合を考慮したセキュリティプロトコルの自動設計の方法について考察した。またSpi-calculnsを用いて、型解析による公開鍵暗号方式を用いるセキュリティプロトコルの相手認証に関する安全性の検証方法について考察した。
2.セキュリティモデルに基づくセキュリティ検査方法 Javaのオブジェクトモデルに適合するような、ローカルな計算資源へのアクセスを管理するためのセキュリティモデルを構築した。また、それに基づき、Javaのソースコードを、ローカルな資源へのアクセス違反を発見するようなソースコードに変換する変換系を設計し、実装した。さらに、DoS攻撃に対するプロトコルの耐性の解析として、コストを考慮した計算体系Spice-calculusを提唱し、型解析による基本的な解析手法を与えた。
さらに、誤りのないシステムの構築のための解析方式と合成方式について以下の結果を得た。
3.リアクティブシステムの仕様解析とシステム合成 時間論理によるリアクティブシステム仕様の実現可能性に係わる様々な性質の検証における状態爆発を押さえるために、状態遷移について、ある時刻については、場合分けをせず、その集合全体を表す時間論理式を持つ集合をノードとしてグラフ表現を行い、状態の場合分けについては、BDDと呼ばれる特殊なデータ構造を用いて表現と操作の双方の効率化を計り、分割検証の新たな方法と組み合わせることによって、他の有名なモデル検査器を流用するより、はるかに効率的であることを実験により実証した。さらに、仕様がプログラム化可能であるための必要条件のうち特に段階的充足可能性を仕様が満たさない原因を形式的に定義し、その導出手続きを構成した。
4.ハードウェア検証方式 回路合成も形式的検証もそのアルゴリズムの中心となるのは状態空間探索であるが、ここでは、信号変化の依存性の情報を利用することにより、状態生成を大幅に削減できる合成・検証手法を開発した。現在までに得られている予備実験の結果では、従来の方法に比べて、10倍から1000倍の高速化が得られており、実用規模の回路への適用が可能となりつつある。

研究成果

• [文献書誌] E.Mercer, C.Myers, T.Yoneda: "Improved poset timing analysis in timed Petri nets"Proc. of The 10th Workshop on Synthesis And System Integration of Mixed Technologies. 127-134 (2001)
• [文献書誌] B.Zhou, T.Yoneda, C.Myers: "Framework of Timed Trace Theoretic Verification Revisited"Pcoc. of 10th Asian Test Symposium. 437-442 (2001)
• [文献書誌] T.Kitai, T.Yoneda: "Partial order reduction in verification of wheel structured parameterized circuits"Proc. of 2001 Pacific Rim International Symposium on Dependable Computing. 173-182 (2001)
• [文献書誌] 北井智也, 米田友洋: "timedシステムの検証におけるfailure tranceの解析に関する研究"FTC研究会資料. (2002)
• [文献書誌] 北井智也, 米田友洋: "Failure trace解析に基づくGasP回路の形式的検証"電子情報通信学会技術研究報告. (掲載予定).
• [文献書誌] Y.Morihiro, T.Yoneda: "Formal Verification of Data-Path Circuits based on Symbolic Simulation"電子情報通信学会英文論文誌. (掲載予定).
• [文献書誌] T.Aoshima, K.Sakuma, N.Yonezaki: "An efficient verification procedure supporting evolution of reactive system specifications"International Workshop on Principles of Software Evolution 2001. (2001)
• [文献書誌] N.Izumi, N.Yonezaki: "A logic of ontology for object oriented software component"Proceedings of The 11th European-Japanese conference on Information Modelling and Knowledge Basis. 74-89 (2001)
• [文献書誌] N.Naoki, N.Yonezaki: "Mereology with class hierarchy for component structure"Proceedings of the IASTED International Conference Artificial Intelligence and Soft Computing. 79-84 (2001)
• [文献書誌] K.Masui, M.Tomoishi, N.Yonezaki: "Design of UNIX system for the prevention of damage propagation by intrusion"Proceedings of Information Security Conference, Lecture Notes in Computer Science 2200. 2200. 536-552 (2001)
• [文献書誌] 讃井崇喜, 萩原茂樹, 米崎直樹: "セキュリティプロトコルの自動設計アルゴリズム"日本ソフトウェア科学会第18回大会講演論文集. (CD-ROM). (2001)
• [文献書誌] 青島武伸, 米崎直樹: "PrestateとBDDを用いたリアクティブシステム仕様の分割検証"日本ソフトウェア科学会第18回大会講演論文集. (CD-ROM). (2001)
• [文献書誌] 増井健司, 友石正彦, 米崎直樹: "パスワードクラック防止のためのunixのパスワードシステムの改善"情報処理学会第62回全国大会論文集. (CD-ROM). (2001)
• [文献書誌] 増井健司, 友石正彦, 米崎直樹: "送受信メッセージのパターン解析によるhttpアクセス制御"日本ソフトウェア科学会第18回大会講演論文集. (CD-ROM). (2001)
• [文献書誌] 増井健司, 友石正彦, 米崎直樹: "送受信内容の相関を利用したhttpアクセス制御のためのプロキシ"マルチメディア、分散、協調とモバイル(DICOM02001)シンポジウム論文集. 669-674 (2001)
• [文献書誌] 畑山研, 萩原茂樹, 米崎直樹: "Spi-calculusを用いたプロトコルの認証に関する性質の検証"日本ソフトウェア科学会第18回大会講演論文集. (CD-ROM). (2001)
• [文献書誌] Noriaki Yoshiura: "Evolution Mechanism of Reactive System Programs"Proc. of International Workshop on Principles of Software Evolution 2001. (2001)
• [文献書誌] N.Yoshiura, N.Yonezaki: "Provability of relevant logic ER"Proceedings of The 11th European-Japanese conference on Information Modelling and Knowledge Basis. 90-104 (2001)
• [文献書誌] 吉浦紀晃, 米崎直樹: "リアクティブシステムの段階的充足可能性とSafety Propertyの関係"信学技報. SS2000-43. 9-16 (2001)
• [文献書誌] 吉浦紀晃: "リアクティブシステムの利用に伴う進化"信学技報. SS2001-13. 9-16 (2001)
• [文献書誌] 吉浦紀晃: "環境に合わせて最適な動作を行うリアクティブシステム"第18回日本ソフトウェア科学会全国大会講演論文集. (CD-ROM). (2001)
• [文献書誌] 吉浦紀晃: "DNSサーバの分散管理から集中管理への移行"情報処理学会、分散システム/インターネット運用技術研究会. (2001)