Research on attack probability using formal methods

2018 Fiscal Year Final Research Report

• Project/Area Number: 16K00196
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Research Field: Information security
• Research Institution: Institute of Information Security
• Principal Investigator: Okubo Takao 情報セキュリティ大学院大学, その他の研究科, 教授 (80417518)
• Project Period (FY): 2016-04-01 – 2019-03-31
• Keywords: 形式手法 / モデル検査 / セキュリティ / リスク評価 / 攻撃可能性

Outline of Final Research Achievements

In this research, in order to evaluate the security risk to the system / software under development, I have modeled the target system formally, and verified the attack possibility using the formal method to evaluate the risk within the development phases. It was found that it is possible to verify the possibility of attack using formal methods such as SPIN, Proverif and EVENT-B by setting a certain vulnerability model. However, when dealing with specific vulnerabilities, it turned out that the vulnerabilities have to be explicitly embedded to the target model.

Free Research Field

脅威分析、セキュリティバイデザイン

Academic Significance and Societal Importance of the Research Achievements

本研究は、攻撃可能性をシステムのセキュリティリスク評価に検討できる可能性を示した。モデル検査を用いた形式手法を用いる場合は、設計仕様などをもとにモデル検査記述言語で対象システムの脆弱性を明示的にモデル化することで、リスク評価が可能になる。その他、未知脆弱性を扱う場合は、脅威分析におけるアタックツリーの妥当性を評価し、再構築すること、あるいは攻撃可能性を機械学習によって示すことで、一定のリスク評価が可能であることを示した。