サイドチャネル攻撃耐タンパ性のためのプログラム検証・プログラム合成技術

2021 年度 研究成果報告書

• 研究課題/領域番号: 18K19787
• 研究種目: 挑戦的研究(萌芽)
• 配分区分: 基金
• 審査区分: 中区分60:情報科学、情報工学およびその関連分野
• 研究機関: 早稲田大学
• 研究代表者: 寺内 多智弘 早稲田大学, 理工学術院, 教授 (70447150)
• 研究期間 (年度): 2018-06-29 – 2022-03-31
• キーワード: サイドチャネル攻撃 / 耐タンパ性 / プログラム検証 / プログラム合成 / 情報セキュリティ

研究成果の概要

Bucketingというタイミング攻撃に対する防衛手段によって得られる安全性およびその限界についての研究を行い成果を得た。確率的adaptiveなである一般的なサイドチャネル攻撃に対する安全性を議論するためのゲーム理論に基づく枠組みを提案した。Spectre攻撃、ReDoS攻撃といった代表的なタイミング攻撃についての研究を行った。加えて、一階述語不動点論理による時相仕様検証、述語制約による関係的仕様の検証、循環証明による分離論理のための定理証明、必勝戦略合成による量化子を含む一階述語論理式の真偽性判定に関する研究など、関連する一般的なプログラム検証および定理証明についての研究も行った。

自由記述の分野

コンピュータサイエンス

研究成果の学術的意義や社会的意義

Bucketingによるタイミング攻撃防衛手法の安全性について初めて形式的な保証を得ることや、確率的かつadaptiveなサイドチャネル攻撃に対する一般的な安全性の議論を可能とするゲーム理論に基づく枠組みを構築するなど、本研究はこれまでのプログラミング言語・形式検証によるセキュリティの研究を大きく飛躍させた。よって、本研究の成果は極めて高い学術的および社会的意義を持つと考える。