2019 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 – 2021-03-31
|
| Keywords | サイドチャネル攻撃 / 耐タンパ性 / プログラム検証 / プログラム合成 / 情報セキュリティ |
|---|
| Outline of Annual Research Achievements |
代表的なサイドチャネル攻撃の一つであるタイミング攻撃に関する研究を行った。具体的には、bucketingというプログラム変換によるタイミング攻撃に対する防衛手法について研究を行った。この研究ではどのようなプログラムおよび攻撃者に対してbucketingが有効であるのか調査することを目指し、bucketingにより安全性の保証を得るための必要条件および十分条件に関する成果を得た。これら、必要条件・十分条件は解析対象システムの正規チャネルとサイドチャネルの安全性を分離して議論することを可能とする枠組みであり、また、過去の観測に依存した動作を行える強力なadaptiveな攻撃者を考慮している。この研究の成果をまとめた論文はセキュリティに関する国際会議The 8th International Conference on Principles of Security and Trust (POST 2019)に採録された。
また、確率的かつadaptiveな攻撃者に対する安全性を議論するためのゲーム理論に基づく枠組みについて研究を行った。具体的には、n-round r-confidenceゲームという新たなゲームを提案し、このゲームが確率的かつadaptiveな攻撃に対する安全性を正確に表現することを証明した。この研究の成果をまとめた論文はセキュリティに関する国際会議The 32nd IEEE Computer Security Foundations Symposium (CSF 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
研究はおおむね順調に進展している。「研究実績の概要」で述べたとおり、今年度はタイミング攻撃に関する研究を行い成果を得た。また、より一般的な確率的かつadaptiveな攻撃に対する安全性を議論するための枠組みについても研究を行い成果を得た。
加えて、定理証明などプログラム検証・プログラム合成のための基盤技術の研究において成果を得た。今回は、特にサイドチャネル攻撃に関する研究として主にタイミング攻撃に限定して成果をあげたが、研究で得られた知見は電力解析など他のサイドチャネル攻撃にも一般化できると期待される。
|
| Strategy for Future Research Activity |
前年度および今年度の研究で得られた知見を元に研究を推進する。以下のテーマに取り組む計画である：(1)タイミング攻撃防衛に関する研究の深化、(2)self-compositionやproduct programなど、セキュリティの自動検証手法に関する研究。
(1)では、bucketingによるタイミング防衛手法により得られる安全性のより厳密な必要条件・十分条件の導出および他のサイドチャネル攻撃に対する防衛手法への一般化などを目指す。(2)では、self-compositionやproduct programなど情報漏洩の検証のための検証手法の拡張を目指す。特に、POST2019の論文ではbucketingを適用したプログラムのタイミング攻撃に対する対タンパ性の検証をself-composition/product program等の手法で検証できるk-safety問題に帰着できることを示した。この結果をもとにした、bucketingを用いたタイミング攻撃に対する対タンパ性の検証手法の確立を目指す。また、self-composition/product program等k-safety問題検証手法と帰納的定理の自動証明などプログラム検証・プログラム合成のための基盤技術の研究との関連性についても研究を行う。加えて、電力解析などのサイドチャネル攻撃に対して有効な防衛手段であるleakage resilienceについての研究なども行う。
|
| Causes of Carryover |
有償ソフトウェア・サービスの代わりに無償ソフトウェア・サービスの利用、早めの航空券購入、および新型コロナウィルス感染症に関する自粛要請による出張取り止めなどの理由により次年度使用額が生じた。当該助成金は翌年度分として請求した助成金と合わせて、研究資料購入など物品費および(可能な状況となれば)国内外の学会参加および共同研究者との打ち合わせなど旅費として使用する計画である。
|
