2020 Fiscal Year Research-status 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 |
代表的なサイドチャネル攻撃の一つであるタイミング攻撃に関する研究を行った。具体的には、bucketingというプログラム変換によるタイミング攻撃に対する防衛手法について研究を行った。この研究ではどのようなプログラムおよび攻撃者に対してbucketingが有効であるのか調査することを目指し、bucketingにより安全性の保証を得るための必要条件および十分条件に関する成果を得た。これら、必要条件・十分条件は解析対象システムの正規チャネルとサイドチャネルの安全性を分離して議論することを可能とする枠組みであり、また、過去の観測に依存した動作を行える強力なadaptiveな攻撃者を考慮している。こちらは、昨年度にセキュリティに関する国際会議The 8th International Conference on Principles of Security and Trust (POST 2019)にて成果を発表した研究を継続し発展させたものである。具体的には、POST 2019で提案した条件を強化することにより、より多くのプログラムに対して、より強い安全性の保証が可能となった。また、本手法の枠組みで得られる保証の理論的限界についても研究を行った。
加えて、一階述語不動点論理による時相仕様検証、述語制約による関係的仕様の検証、循環証明による分離論理のための定理証明や必勝戦略合成による量化子を含む一階述語論理式の真偽性判定に関する研究など、関連するより一般的なプログラム検証および定理証明についての研究も行った。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究はおおむね順調に進展している。「研究実績の概要」で述べたとおり、今年度はタイミング攻撃に関する研究を行い成果を得た。
加えて、定理証明などプログラム検証・プログラム合成のための基盤技術の研究において成果を得た。今回は、特にサイドチャネル攻撃に関する研究として主にタイミング攻撃に限定して成果をあげたが、研究で得られた知見は電力解析など他のサイドチャネル攻撃にも一般化できると期待される。
|
| Strategy for Future Research Activity |
これまでの研究で得られた知見を元に研究を推進する。具体的には、以下のテーマに取り組む計画である：(1)bucketingによるタイミング攻撃防衛に関する理論的研究の深化、(2)Spectre攻撃などタイミング攻撃を用いたセキュリティ攻撃の研究、(3)関係的仕様などセキュリティに関する仕様の自動検証手法の研究、(4)ReDoS攻撃など正規表現を含むプログラムに対するセキュリティ攻撃に関する研究。
(1)では、bucketingによるタイミング防衛手法により得られる安全性のより厳密な必要条件・十分条件の導出を目指す。また、その限界性についても引き続き研究を行う。(2)では、投機的実行による実行時間の差を用いるSpectre攻撃などタイミングチャネルを用いた高度なセキュリティ攻撃に対する防衛手段について研究を行う。(3)ではself-compositionを用いた関係的仕様の自動検証手法の研究、およびそのような手法を応用したセキュリティに関する仕様の自動検証手法について研究を行う。(4)では、ReDoS攻撃など正規表現を含むプログラムに対するDoS(denial of service)攻撃に関する研究を行う。
|
| Causes of Carryover |
有償ソフトウェア・サービスの代わりに無償ソフトウェア・サービスの利用、および新型コロナウィルス感染症に関する自粛要請による出張取り止めなどの理由により次年度使用額が生じた。当該助成金は翌年度分として、研究資料購入など物品費および(可能な状況となれば)国内外の学会参加および共同研究者との打ち合わせなど旅費として使用する計画である。
|
