2022 Fiscal Year Research-status Report

ネットワークシステムのセキュリティで等価な仮想評価環境の構築

Research Project

Project/Area Number	22K11982
Research Institution	Tokyo University of Technology
Principal Investigator	布田裕一東京工科大学, コンピュータサイエンス学部, 教授 (50706223)
Co-Investigator(Kenkyū-buntansha)	岡崎裕之信州大学, 学術研究院工学系, 准教授 (50432167) 鈴木彦文信州大学, 学術研究院総合人間科学系, 准教授 (30300578)
Project Period (FY)	2022-04-01 – 2026-03-31
Keywords	セキュリティ評価 / 仮想化技術 / DDoS攻撃 / 観測等価性
Outline of Annual Research Achievements	本研究の対象であるネットワークのシステムに対するセキュリティ評価において、DDoS攻撃を実際のネットワーク（実機環境）を用いて発生させると影響が大きく頻繁に評価ができないため、仮想環境を用いた評価環境を構築している。しかし、仮想環境を用いた評価結果は、実機環境を用いた評価結果に比べ信頼性が十分であるとはいえない。令和4年度は研究課題1：仮想ルータ／サーバと実機ルータ／サーバのセキュリティ的な違いの抽出と、研究課題2：仮想モデルと実機モデルの観測等価性の判定フレームワークの構築に取り組んだ。研究課題1に関して、DoS攻撃の一種であるTCP Flood攻撃によるUTMがダウンしてしまう状況を仮想化技術を用いて再現する評価環境において、仮想ルータで通信のボトルネックとなっている課題をDPDK(Data Plane Development Kit)を用いて改善するべく取り組んだ。また、様々なシステムに対するDoS攻撃を評価するため、仮想化技術を用いた制御システムに対して正常通信を偽装する攻撃評価環境の構築、検知方法の考案及び評価を実施した。さらに、DoS 攻撃を用いた脆弱な WPA2-Enterprise AP に対する2段階 EvilTwin 攻撃を考案し、安全性を検証した。研究課題2に関しては、仮想環境を用いてDDoS攻撃評価を行う際には、評価結果の信頼度が仮想環境と実環境間のギャップに依存する。そこで仮想環境と実環境をそれぞれ形式モデル化して、そのギャップをモデル検査技術によって評価する手法の開発を進めている。令和4年度は評価に利用する形式検証ツールの選定を行うために、安全性検証用の主要なツールであるProVerifとTamarin双方でAEADの形式検証を行って、それぞれの形式記述の表現力と、検証性能の比較及び評価を行った。
Current Status of Research Progress	Current Status of Research Progress 2: Research has progressed on the whole more than it was originally planned. Reason 令和4年度の目標は、研究課題1におけるDDoS攻撃の攻撃評価環境に含まれる仮想ルータや仮想サーバと、実機ルータや実機サーバの動作の違いの抽出と、攻撃評価への影響の分析であった。これについては、仮想ルータやサーバを用いた攻撃評価環境の性能強化を実施しているが、影響の分析までには至っていない。しかし、仮想環境を用いた攻撃評価環境を制御システムに展開した。また、研究課題2の検討を先に実施しており、仮想環境と実環境をそれぞれ形式モデル化して、そのギャップをモデル検査技術によって評価する手法の開発を進めている。以上より総合的には「おおむね順調に進展」と判断した。
Strategy for Future Research Activity	研究課題1に関しては、仮想化技術を用いたDDoS攻撃の攻撃評価環境のDPDKを用いた性能強化と、詳細な攻撃評価及び実機環境との比較を継続で実施し、動作の違いを吸収する模倣方法を検討する。また、様々なシステムに対するDoS攻撃を評価する目的で、制御システムや無線LANなどのDoS攻撃の評価環境の構築と評価も実施する。研究課題2に関しては、令和4年度に比較評価を実施した二つの主要な安全性形式検証ツール、ProVerifおよびTamarinのうちのProVerifを主として利用して検証手法の開発を進める。これは二つの検証ツールそれぞれの特徴が異なり、本研究課題の目的である二つの環境間の形式モデルのふるまいの違いを評価することにProVerifが向いていることが判明したためである。そこで具体的に、検索可能暗号サーバの理想モデルと現実モデルの形式化を行って、その形式的安全性を進める。
Causes of Carryover	検証環境の構築用計算機で使用するPC部品の一部を購入する予定であったが、他の部品も含めて令和5年度に購入し計算機を作成するように変更したためである。令和4年度の購入予定分のPC部品と令和5年度に購入するPC部品も併せて購入していく。研究打ち合わせや学会発表による予算執行は予定通り進める。