2018 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)に採録された。
加えて、一階述語不動点論理による時相仕様検証や循環証明による分離論理のための定理証明など、関連するより一般的なプログラム検証および定理証明についての研究も行った。
|
| 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)タイミング攻撃防衛に関する研究の深化、(2)adaptiveなサイドチャネル攻撃に関する研究。具体的に、(1)ではbucketingによるタイミング防衛手法により得られる安全性のより厳密な必要条件・十分条件の導出および他のサイドチャネル攻撃に対する防衛手法への一般化などを目指す。(2)ではadaptiveなサイドチャネル攻撃に関して一般的な議論を行うための枠組みの構築などを目指す。加えて、電力解析などのサイドチャネル攻撃に対して有効な防衛手段であるleakage resilienceについての研究なども行う。
|
| Causes of Carryover |
有償ソフトウェア・サービスの代わりに無償ソフトウェア・サービスの利用および早めの航空券購入などにより次年度使用額が生じた。当該助成金は翌年度分として請求した助成金と合わせて、国内外の学会参加および共同研究者との打ち合わせなど旅費および、研究資料購入など物品費として使用する計画である。
|
