Program verification and program synthesis for side-channel attack resilience

2021 Fiscal Year Final Research Report

• Project/Area Number: 18K19787
• Research Category: Grant-in-Aid for Challenging Research (Exploratory)
• Allocation Type: Multi-year Fund
• Review Section: Medium-sized Section 60:Information science, computer engineering, and related fields
• Research Institution: Waseda University
• Principal Investigator: Terauchi Tachio 早稲田大学, 理工学術院, 教授 (70447150)
• Project Period (FY): 2018-06-29 – 2022-03-31
• Keywords: サイドチャネル攻撃 / 耐タンパ性 / プログラム検証 / プログラム合成 / 情報セキュリティ

Outline of Final Research Achievements

We have conducted a research on a formal analysis of a timing channel attack mitigation technique called "bucketing". We have obtained results on provable security guarantees achievable with the technique as well as its theoretical limits. We have proposed a game theoretic general framework for proving security of a system against probabilistic and adaptive side channel attacks. We have conducted research on Spectre attacks and ReDoS attacks which are popular timing attacks. Additionally, we have conducted research on more general program verification and automated deduction, including temporal property verification by first-order fixpoint logic solving, relational property verification by predicate constraint solving, type and effect systems for algebraic effects and handlers, and automated deduction for quantified formulas by game solving.

Free Research Field

コンピュータサイエンス

Academic Significance and Societal Importance of the Research Achievements

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