2001 Fiscal Year Annual Research Report

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

Research Project

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

Research Products
(22 results)

All Other

All Publications (22 results)

[Publications] 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)
[Publications] B.Zhou, T.Yoneda, C.Myers: "Framework of Timed Trace Theoretic Verification Revisited"Pcoc. of 10th Asian Test Symposium. 437-442 (2001)
[Publications] 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)
[Publications] 北井智也, 米田友洋: "timedシステムの検証におけるfailure tranceの解析に関する研究"FTC研究会資料. (2002)
[Publications] 北井智也, 米田友洋: "Failure trace解析に基づくGasP回路の形式的検証"電子情報通信学会技術研究報告. (掲載予定).
[Publications] Y.Morihiro, T.Yoneda: "Formal Verification of Data-Path Circuits based on Symbolic Simulation"電子情報通信学会英文論文誌. (掲載予定).
[Publications] 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)
[Publications] 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)
[Publications] 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)
[Publications] 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)
[Publications] 讃井崇喜, 萩原茂樹, 米崎直樹: "セキュリティプロトコルの自動設計アルゴリズム"日本ソフトウェア科学会第18回大会講演論文集. (CD-ROM). (2001)
[Publications] 青島武伸, 米崎直樹: "PrestateとBDDを用いたリアクティブシステム仕様の分割検証"日本ソフトウェア科学会第18回大会講演論文集. (CD-ROM). (2001)
[Publications] 増井健司, 友石正彦, 米崎直樹: "パスワードクラック防止のためのunixのパスワードシステムの改善"情報処理学会第62回全国大会論文集. (CD-ROM). (2001)
[Publications] 増井健司, 友石正彦, 米崎直樹: "送受信メッセージのパターン解析によるhttpアクセス制御"日本ソフトウェア科学会第18回大会講演論文集. (CD-ROM). (2001)
[Publications] 増井健司, 友石正彦, 米崎直樹: "送受信内容の相関を利用したhttpアクセス制御のためのプロキシ"マルチメディア、分散、協調とモバイル(DICOM02001)シンポジウム論文集. 669-674 (2001)
[Publications] 畑山研, 萩原茂樹, 米崎直樹: "Spi-calculusを用いたプロトコルの認証に関する性質の検証"日本ソフトウェア科学会第18回大会講演論文集. (CD-ROM). (2001)
[Publications] Noriaki Yoshiura: "Evolution Mechanism of Reactive System Programs"Proc. of International Workshop on Principles of Software Evolution 2001. (2001)
[Publications] 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)
[Publications] 吉浦紀晃, 米崎直樹: "リアクティブシステムの段階的充足可能性とSafety Propertyの関係"信学技報. SS2000-43. 9-16 (2001)
[Publications] 吉浦紀晃: "リアクティブシステムの利用に伴う進化"信学技報. SS2001-13. 9-16 (2001)
[Publications] 吉浦紀晃: "環境に合わせて最適な動作を行うリアクティブシステム"第18回日本ソフトウェア科学会全国大会講演論文集. (CD-ROM). (2001)
[Publications] 吉浦紀晃: "DNSサーバの分散管理から集中管理への移行"情報処理学会、分散システム/インターネット運用技術研究会. (2001)

2001 Fiscal Year Annual Research Report

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

Principal Investigator

米崎 直樹 東京工業大学, 大学院・情報理工学研究科, 教授 (00126286)

Research Products

[Publications] 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)

[Publications] B.Zhou, T.Yoneda, C.Myers: "Framework of Timed Trace Theoretic Verification Revisited"Pcoc. of 10th Asian Test Symposium. 437-442 (2001)

[Publications] 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)

[Publications] 北井智也, 米田友洋: "timedシステムの検証におけるfailure tranceの解析に関する研究"FTC研究会資料. (2002)

[Publications] 北井智也, 米田友洋: "Failure trace解析に基づくGasP回路の形式的検証"電子情報通信学会技術研究報告. (掲載予定).

[Publications] Y.Morihiro, T.Yoneda: "Formal Verification of Data-Path Circuits based on Symbolic Simulation"電子情報通信学会英文論文誌. (掲載予定).

[Publications] 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)

[Publications] 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)

[Publications] 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)

[Publications] 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)

[Publications] 讃井崇喜, 萩原茂樹, 米崎直樹: "セキュリティプロトコルの自動設計アルゴリズム"日本ソフトウェア科学会第18回大会講演論文集. (CD-ROM). (2001)

[Publications] 青島武伸, 米崎直樹: "PrestateとBDDを用いたリアクティブシステム仕様の分割検証"日本ソフトウェア科学会第18回大会講演論文集. (CD-ROM). (2001)

[Publications] 増井健司, 友石正彦, 米崎直樹: "パスワードクラック防止のためのunixのパスワードシステムの改善"情報処理学会第62回全国大会論文集. (CD-ROM). (2001)

[Publications] 増井健司, 友石正彦, 米崎直樹: "送受信メッセージのパターン解析によるhttpアクセス制御"日本ソフトウェア科学会第18回大会講演論文集. (CD-ROM). (2001)

[Publications] 増井健司, 友石正彦, 米崎直樹: "送受信内容の相関を利用したhttpアクセス制御のためのプロキシ"マルチメディア、分散、協調とモバイル(DICOM02001)シンポジウム論文集. 669-674 (2001)

[Publications] 畑山研, 萩原茂樹, 米崎直樹: "Spi-calculusを用いたプロトコルの認証に関する性質の検証"日本ソフトウェア科学会第18回大会講演論文集. (CD-ROM). (2001)

[Publications] Noriaki Yoshiura: "Evolution Mechanism of Reactive System Programs"Proc. of International Workshop on Principles of Software Evolution 2001. (2001)

[Publications] 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)

[Publications] 吉浦紀晃, 米崎直樹: "リアクティブシステムの段階的充足可能性とSafety Propertyの関係"信学技報. SS2000-43. 9-16 (2001)

[Publications] 吉浦紀晃: "リアクティブシステムの利用に伴う進化"信学技報. SS2001-13. 9-16 (2001)

[Publications] 吉浦紀晃: "環境に合わせて最適な動作を行うリアクティブシステム"第18回日本ソフトウェア科学会全国大会講演論文集. (CD-ROM). (2001)

[Publications] 吉浦紀晃: "DNSサーバの分散管理から集中管理への移行"情報処理学会、分散システム/インターネット運用技術研究会. (2001)

米崎直樹東京工業大学, 大学院・情報理工学研究科, 教授 (00126286)