| 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
|
| Project Status |
Completed (Fiscal Year 2018)
|
| Budget Amount *help |
¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000)
Fiscal Year 2018: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000)
Fiscal Year 2017: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2016: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
|
|---|
| Keywords | 形式手法 / モデル検査 / セキュリティ / リスク評価 / 攻撃可能性 / アタックツリー / 到達可能性 / Webアプリケーション / 機械学習 / 攻撃可能性評価 / 知識ベース / 分析効率化 / CAPEC / CWE / セーフティ / 攻撃モデル / 攻撃解析 / ソフトウェア開発 |
|---|
| 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.
|
| Academic Significance and Societal Importance of the Research Achievements |
本研究は、攻撃可能性をシステムのセキュリティリスク評価に検討できる可能性を示した。モデル検査を用いた形式手法を用いる場合は、設計仕様などをもとにモデル検査記述言語で対象システムの脆弱性を明示的にモデル化することで、リスク評価が可能になる。その他、未知脆弱性を扱う場合は、脅威分析におけるアタックツリーの妥当性を評価し、再構築すること、あるいは攻撃可能性を機械学習によって示すことで、一定のリスク評価が可能であることを示した。
|
