2021 Fiscal Year Annual Research Report
Program verification and program synthesis for side-channel attack resilience
| Project/Area Number |
18K19787
|
|---|
| Research Institution | Waseda University |
|---|
Principal Investigator |
寺内 多智弘 早稲田大学, 理工学術院, 教授 (70447150)
|
|---|
| Project Period (FY) |
2018-06-29 – 2022-03-31
|
| Keywords | サイドチャネル攻撃 / 耐タンパ性 / プログラム検証 / プログラム合成 / 情報セキュリティ |
|---|
| Outline of Annual Research Achievements |
これまでのサイドチャネル攻撃に関する基礎的研究で得られた知見を元に、タイミング攻撃を用いた代表的な攻撃手段であるSpectre攻撃およびRegular expression Denial of Service (ReDoS)攻撃に関する研究を行った。Spectre攻撃に関しては、近年speculative non-interference, weak speculative non-interference, speculative constant-time-securityなど多数の形式的定義が提案されており、それぞれの利点・問題点を明らかにする研究を行った。また、静的コード解析によるSpectre攻撃脆弱性の検出についても研究を行った。ReDoS攻撃に関しては、後方参照・先読み後読みなどの機能で拡張された拡張正規表現のReDoS脆弱性を修正する手法について研究を行った。
加えて、一階述語不動点論理による時相仕様検証、代数的エフェクト・ハンドラを含むプログラムのための時相仕様検証、述語制約解消による関係的仕様の検証など、関連するより一般的なプログラム検証および定理証明についての研究も行った。代数的エフェクト・ハンドラを含むプログラムのための時相仕様検証に関しては、成果をまとめた論文がプログラミング言語分野の国内会議プログラミングおよびプログラミング言語ワークショップに採録された。述語制約解消による関係的仕様の検証については、成果をまとめた論文が形式検証分野の最高峰の国際会議であるInternational Conference on Computer Aided Verification (CAV)に採録された。
|
-
[Journal Article] Constraint-Based Relational Verification2021
Author(s)
Hiroshi Unno, Tachio Terauchi, and Eric Koskinen
-
Journal Title
In Proceedings of the 33rd International Conference on Computer-Aided Verification (CAV 2021), Lecture Notes in Computer Science 12759
Volume: 1
Pages: 742～766
DOI
Peer Reviewed / Open Access / Int'l Joint Research
-
-
-
