2024-03-29T23:16:28Zhttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_oaipmhoai:ipsj.ixsq.nii.ac.jp:001468302023-11-14T00:51:14Z06164:06165:06462:08443
形式検証を用いた攻撃分析フレームワークの提案Proposal of Attack Analysis Framework Using Formal VerificationjpnCSS,形式検証,攻撃分析http://id.nii.ac.jp/1001/00146797/Conference Paperhttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_action_common_download&item_id=146830&item_no=1&attribute_id=1&file_no=1Copyright (c) 2015 by the Information Processing Society of Japan情報セキュリティ大学院大学神奈川大学早稲田大学国立情報学研究所大久保, 隆夫海谷, 治彦鷲崎, 弘宣吉岡, 信和プロトコルなどの仕様の誤り,ないし仕様の誤った実装によるソフトウェア脆弱性や,脆弱性をついた攻撃が問題となっている.また,ソフトウェアを安全にするためには技術的対策だけではなく,運用時に人的な管理策が必要となる場合もある.本稿では,ソフトウェアの開発の途中段階あるいはプロトコルの実装段階を,脆弱性や外部環境に依存する形式でモデル化し,段階が進んだ時に脆弱性により攻撃が可能になるかどうかを,脆弱性や外部環境によりモデルを変化させつつ形式検証により検査するフレームワークを提案する.更に,提案フレームワークを用いれば検査の結果,開発や運用の際に防がなければならない脆弱性や管理策が明らかになることを示す.There are numbers of security incidents because of attacks exploiting vulnerability of the wrong implementation of a protocol, or because of the error of the protocol itself. Some software requires management methods for security. In this paper we propose a formal verification for checking attack potential of the intermediate state of developing software, using formal model depending on conditions or environments for security.コンピュータセキュリティシンポジウム2015論文集201532822892015-10-142015-12-18