Program verification and program synthesis for side-channel attack resilience
| 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 |
|
|---|
| Project Period (FY) |
2018-06-29 – 2022-03-31
|
| Project Status |
Completed (Fiscal Year 2021)
|
| Budget Amount *help |
¥6,240,000 (Direct Cost: ¥4,800,000、Indirect Cost: ¥1,440,000)
Fiscal Year 2020: ¥2,080,000 (Direct Cost: ¥1,600,000、Indirect Cost: ¥480,000)
Fiscal Year 2019: ¥2,080,000 (Direct Cost: ¥1,600,000、Indirect Cost: ¥480,000)
Fiscal Year 2018: ¥2,080,000 (Direct Cost: ¥1,600,000、Indirect Cost: ¥480,000)
|
|---|
| 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.
|
| Academic Significance and Societal Importance of the Research Achievements |
Bucketingによるタイミング攻撃防衛手法の安全性について初めて形式的な保証を得ることや、確率的かつadaptiveなサイドチャネル攻撃に対する一般的な安全性の議論を可能とするゲーム理論に基づく枠組みを構築するなど、本研究はこれまでのプログラミング言語・形式検証によるセキュリティの研究を大きく飛躍させた。よって、本研究の成果は極めて高い学術的および社会的意義を持つと考える。
|
Report
(5 results)
Research Products
(16 results)
-
-
-
-
[Journal Article] A Formal Analysis of Timing Channel Security via Bucketing2019
Author(s)
Terauchi Tachio, Antonopoulos Timos
-
Journal Title
In Proceedings of the 8th International Conference on Principles of Security and Trust (POST 2019), Lecture Notes in Computer Science
Volume: 11426
Pages: 29-50
DOI
ISBN
9783030171377, 9783030171384
Related Report
Peer Reviewed / Open Access / Int'l Joint Research
-
-
-
-
-
-
-
-
-
-
-
-
