| 研究実績の概要 |
これまでのサイドチャネル攻撃に関する基礎的研究で得られた知見を元に、タイミング攻撃を用いた代表的な攻撃手段である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)に採録された。
|
