2018 Fiscal Year Annual Research Report
Research on attack probability using formal methods
| Project/Area Number |
16K00196
|
|---|
| Research Institution | Institute of Information Security |
|---|
Principal Investigator |
大久保 隆夫 情報セキュリティ大学院大学, その他の研究科, 教授 (80417518)
|
|---|
| Project Period (FY) |
2016-04-01 – 2019-03-31
|
| Keywords | セキュリティ / リスク評価 / 形式手法 / 攻撃可能性 / アタックツリー / 到達可能性 / Webアプリケーション / 機械学習 |
|---|
| Outline of Annual Research Achievements |
本研究では、セキュリティのリスク評価に、ソフトウェアの仕様をモデル化した上で形式的手法が使えないかの検討を行った。自動的に検出可能なモデル検査を用い、ソフトウェアの脆弱性を持つモデルがモデル検査によって検出可能かの検討を行った。検討に際し、いくつかの記述能力の異なる言語を検討した。SPIN/Promela、Proverif、EVENT-B、Alloyなどを使い、一定の脆弱性を設定した上で、その発見にモデル検査が利用できることを確認した。しかし、どの言語においても、モデルに脆弱性を明示的に組み込む必要があることが分かった。これは、本研究において目標としていた、未知の脆弱性を含むモデルについて、その攻撃可能性評価を評価することが困難であることを示す。
形式手法あるいはモデル検査そのものをモデルとしたリスク評価が困難ということが判明したため、本研究では方針を調整し次の2つの方向でリスク評価を検討することとした。
(1)攻撃の要因分析に用いるアタックツリーを用い、リスク評価の精度を高める手法。
この手法では、グラフ化したアタックツリーの中で、最もボトルネックとなっている個所を検出し、リスクの重要性順序付けに用いる手法である。もう一つは、アタックツリーの冗長性や関係性の欠如の有無の評価と最適化を、Interpretive Structural Modeling(ISM)法によって行う手法である。これらは国内ではあまり進んでいないアタックツリー分析の妥当性評価に用いることができると考えられる。
(2)既存のプログラムについて、脆弱性評価を行うテストを機械学習により自動生成する手法の研究
これを、WebアプリケーションのSQLインジェクションに用い、テストを生成することができた。
|
