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

2000 年度 実績報告書

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

研究概要

正しく作られたシステムへの人為的な介入によって、システムの意図がねじ曲げられることを防御するために、設計レベルでの検証方法、実現レベルでの防御法について研究を行い、以下の成果を得た。
・セキュリティープロトコルの攻撃に対する安全性の検証
セキュリティプロトコルの重要な性質として、送信者の状態推定によるメッセージの認証、及びメッセージすり替えの可能性のないことに関する検証を行うための健全な様相論理体系を得た。
・セキュリティ検査方法の構築
実行時に安全性を確保する問題として、Javaの署名付きコードの安全性について研究を行った。すなわち、Javaにおける署名つきコードの安全性の向上を支援するためのソフトウェアツールとして、Javaにおけるインテグリティ解析のためのトランスレータを設計・試作した。
その中で用いられるJavaのオブジェクト指向的な計算機構に適合するインテグリティモデルとして、リファレンスモデルと呼ばれるものを提案した。
また、以下のような動作タイミングが問題となるリアクティブシステムや非同期回路について、厳密な検証技法の適用可能性を拡大する研究を行い、以下の成果を得た。
・仕様記述解析方式の定式化
特に実現可能性に関する仕様の満たすべき性質の効率的検証法について研究を行い、停止性を仮定したシステムに関する完全な検証系を構築すると共に、効率的モジュール検証に、最弱な外部イベント制約式を求める部分評価を用いた効率的検証法を構築し、実験によりその効果を確かめた。
・ハードウェア検証方式
有限幅遅延モデルにおける非同期式回路の検証ツールの公開、およびシミュレーションを利用した同期式回路の形式的検証方式の拡張、車輪状構造をもつスケーラブルシステムの効率的検証方法について評価等を主に行った。
特に、非同期回路の検証方式をVINAS-Pというツールとして実現し、Web上で公開した。

研究成果

• [文献書誌] T.Aoshima,N.Yonezaki: "An efficient tableau-based verification method with partial evaluation for reactive system specifications"Proc.of The 10th European-Japanese Conf.on Information Modelling and Knowledge Bases. 337-348 (2000)
• [文献書誌] V.Vanitha,K.Yamashita,K.Fukuzawa,N.Yonezaki: "A method for structuralisation of evolutional specifications of reactive systems"ICSE 2000, The third International Workshop on Intelligent Software Engineering(WISE3). 30-38 (2000)
• [文献書誌] N.Yoshiura,N.Yonezaki: "Decidable relevant logic ER and its tableau method based decision procedure"Automated Reasoning with Analytic Tableaux and Related Methods. (2000)
• [文献書誌] N.Yoshiura,N.Yonezaki: "Program synthesis for stepwise satisfiable specification of reactive system"International Sympo.on Principles of Software Evolution, ISPSE2000. 55-64 (2000)
• [文献書誌] M.Tomoishi,N.Yonezaki: "Evolutional tableau method for temporal logic specification"International Sympo.on Principles of Software Evolution,ISPSE2000. 181-188 (2000)
• [文献書誌] T.Aoshima,N.Yonezaki: "Verification of reactive system specification with outer event conditional formula"Internatioanl Sympo.on Principles of Software Evolution,ISPSE2000. 195-199 (2000)
• [文献書誌] 増井健司,友石正彦,米崎直樹: "リレーサーバを用いたpop before smtpのセキュアな実現法とその解析"日本ソフトウェア科学会第17回大会講演論文集. (2000)
• [文献書誌] 青島武伸,米崎直樹: "部分評価を用いる時相論理タブロー証明系の効率化"日本ソフトウェア科学会第17回大会講演論文集. (2000)
• [文献書誌] 泉直子,米崎直樹: "オブジェクトの項表現を意味論の基礎とする論理体系としてのontologyとその表現力"人工知能学会全国大会(第14回)論文集. 514-517 (2000)
• [文献書誌] 萩原茂樹,友石正彦,米崎直樹: "有限フレームを意味的基礎として持つ様相論理に対する分解証明法"コンピュータソフトウェア別冊ソフトウェア発展. 78-91 (2000)
• [文献書誌] 根岸和義,米崎直樹: "セキュリティプロトコルにおける暗号化メッセージの送信者による認知に関する検証法"情処研報2000-CSEC-11. 2000-80. 25-30 (2000)
• [文献書誌] 根岸和義,米崎直樹: "並行セッションの情報を用いる攻撃を考慮したプロトコルセキュリティの検証"日本ソフトウェア科学会第17会大会論文集. (2000)
• [文献書誌] 根岸和義,米崎直樹: "セキュリティプロトコルの一貫性および正常終了一致の同一参加者による複数セッションを考慮し検証法"情報処理学会論文誌. 41-8. 2281-2290 (2000)
• [文献書誌] Negishi,K.and Yonezaki,N.: "Verification method for possibility of parallel attack on multiple sessions with the same principals in a security protocol"Informal proceeding of Formal Method on Computer Security 2000. 109-120 (2000)
• [文献書誌] 小黒裕介,岡埜靖,米田友洋: "データパスを含む非同期式回路の検証について"電子情報通信学会技術研究報告FTS-2000. 9. 65-72 (2000)
• [文献書誌] Tomohiro Yoneda: "VINAS-P : A tool for trace theoretic verification of timed asynchronous circuits"Proc.of Computer Aided Verification,LNCS. 1855. 572-575 (2000)
• [文献書誌] Y.Morihiro,T.Yoneda: "Verifying Stacks and Queues Using Symbolic Simulation Techniques"Proc.of 2000 International Workshop on RTL ATPG & DET. 119-128 (2000)
• [文献書誌] M.Saarepera,T.Yoneda: "Implementation of Quasi Delay-Insensitive Boolean Function Blocks"電子情報通信学会英文論文誌. E83-D-10. 1879-1889 (2000)
• [文献書誌] 北井智也,米田友洋: "星状抽象ペトリネットの解析に関する研究"電子情報通信学会技術研究報告FTS-2000. 59. 149-154 (2000)
• [文献書誌] Y.Morihiro,T.Yoneda: "Formal Verification of Data-Path Circuits based on Symbolic Simulation"Proc.of 9th Asian Test Symposium. 329-336 (2000)
• [文献書誌] 森広芳文,米田友洋: "シミュレーションを利用した形式的検証システム"電子情報通信学会和文論文誌D-I分冊掲載予定. (2000)
• [文献書誌] B.Zhou,T.Yoneda: "Conformance and Mirroring for Timed Asynchronous Circuits"Proc of ASP-DAC2001掲載予定. (2000)
• [文献書誌] 児島尚,丸山宏,西崎真也: "Javaにおけるインテグリティモデル"第29回情報処理学会プログラミング研究会. (2000)
• [文献書誌] 児島尚,丸山宏,西崎真也: "Javaにおけるインテグリティモデル"日本ソフトウェア科学会第17回大会. (2000)