2016 Fiscal Year Research-status Report
| Project/Area Number |
16K00196
|
|---|
| Research Institution | Institute of Information Security |
|---|
Principal Investigator |
大久保 隆夫 情報セキュリティ大学院大学, その他の研究科, 教授 (80417518)
|
|---|
| Project Period (FY) |
2016-04-01 – 2019-03-31
|
| Keywords | 形式手法 / モデル検査 / 攻撃モデル / リスク評価 / セキュリティ |
|---|
| Outline of Annual Research Achievements |
平成28年度は，既存の形式記述言語，特にモデル検査対応の言語(SPIN/Promela, Proverif, Event-B)を調査し，セキュリティ問題の検証，特に攻撃の可能性検証に用いることができるかを検討を行った．
Promelaはプロセスとチャネルを用いた通信が可能であるため，Webのようなサーバ，クライアントの自然な表現に適する．ProVerifは，暗号向けの安全性検証ツールである．reachability(到達可能性)や，observational equivalence，non-interferenceなど特性の検証をサポートするが，これらの特性は，攻撃の検証として用いることができると考える．また，observational equivalenceは，ある操作を正規利用者が行ったのか攻撃者が行ったのか識別ができなければ，攻撃が成功することになるので，なりすましや遠隔操作の検証に用いることができると考えられた．Event-Bは，Bメソッドをベースに開発された，要求仕様の形式検証のための言語である．Event-Bでは，初期に定義したモデルを段階的に詳細化するモデルを作成することで，段階的にソフトウェア仕様を詳細化していくたびに，詳細化されたモデルを作成し，そのモデルが元の要求を満たしているかを検証することができる．元の要求は，詳細化前のモデルに不変条件などの形で記述できる．
我々は，検討の結果，Event-Bのリファインメントとそれによる不変条件の変化による証明失敗などを利用して，脅威の検出な可能な抽象レベル，具体レベル双方における脅威のモデル化を実現した．この結果について2017年1月の暗号と情報セキュリティシンポジウムで発表した．
また攻撃のモデル化のため、attack treeの中でクリティカルな部分を抽出する手法を考案し，国内シンポジウムで発表を行った。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
それぞれの形式言語は，攻撃モデルの表現には長所，短所があることが分かった．
Promela/SPINを用いた場合，並列処理やプロセス間通信における攻撃のモデル化には適している一方，基本的には定数しか扱えない上に，記述性が高くないため，攻撃はすべて明示的にプロセス定義によって行う必要があった．
一方，Proverifによるモデル化では，機密性の記述が用意であったり，プロセス数を任意に増やすことができる点が長所として挙げられる．また，関数が記述できるため，脆弱性のふるまいの記述もPromelaよりは容易になる．攻撃の可能性も，reachabilityやobservational equivqlenceを用いることでモデルの記述可能性が高い面もある．しかし，完全性や可用性を直接表現できる仕様がなかったり，機密性の仕様も暗号における機密性に特化しているため，それ以外の特性の記述には工夫が必要となる．
Event-Bは，本提案のようにリファインメントを用いることによって，セキュリティ要件や攻撃，対策を対象のリファインメントとして記述することにより，それぞれを分離して扱うことができる．また，状況に応じて攻撃そのものもリファインメントで詳細化できるため，攻撃によるリスク評価にも用いることができ，脅威分析(attack treeの下位ノードの発見など)の自動化の助けになることが期待できる．
また，いずれの言語においても，脆弱性の表現の仕方は問題が残るころが分かった．開発時に明示的に脆弱性を記述することは比較的可能だが，その方式では隠された脆弱性をつく攻撃の発見という意義が失なわれてしまう．この点については引き続き検討を行う必要がある．
|
| Strategy for Future Research Activity |
現状ではいくつかの攻撃をモデル化した段階となっている．今後は，抽象的な攻撃と，より具体的な攻撃の2つの観点からモデル化を進め，有効性の評価および自動化の検討を行う予定である．
具体的には，CAPECやCWEなどの既存の攻撃，脆弱性データベースから攻撃モデルのためのデータを抽出し，モデル化を行う予定である．
また，これらのデータの機械的適用のため，attack treeなどによるモデル化を合わせて検討する．
|
| Causes of Carryover |
使用計画のうち約27000円については、2月、阪大での研究打ち合わせにて使用する予定だったが、1月の沖縄でのシンポジウムの際に、関係者が会合して打ち合わせができたため、1回分未使用となった。
|
| Expenditure Plan for Carryover Budget |
未使用となった分については、次年度の研究打ち合わせの旅費として使用する予定である。
|
-
-
[Presentation] 非干渉性の再考と応用2017
Author(s)
矢内直人，大久保隆夫
Organizer
暗号と情報セキュリティシンポジウム
Place of Presentation
ホテルロワジール那覇
Year and Date
2017-01-24 – 2017-01-27
-
-
