• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2018 年度 実施状況報告書

サイドチャネル攻撃耐タンパ性のためのプログラム検証・プログラム合成技術

研究課題

研究課題/領域番号 18K19787
研究機関早稲田大学

研究代表者

寺内 多智弘  早稲田大学, 理工学術院, 教授 (70447150)

研究期間 (年度) 2018-06-29 – 2021-03-31
キーワードサイドチャネル攻撃 / 耐タンパ性 / プログラム検証 / プログラム合成 / 情報セキュリティ
研究実績の概要

代表的なサイドチャネル攻撃の一つであるタイミング攻撃に関する研究を行った。具体的には、bucketingというプログラム変換によるタイミング攻撃に対する防衛手法について研究を行った。この研究ではどのようなプログラムおよび攻撃者に対してbucketingが有効であるのか調査することを目指し、bucketingにより安全性の保証を得るための必要条件および十分条件に関する成果を得た。これら、必要条件・十分条件は解析対象システムの正規チャネルとサイドチャネルの安全性を分離して議論することを可能とする枠組みであり、また、過去の観測に依存した動作を行える強力なadaptiveな攻撃者を考慮している。この研究の成果をまとめた論文はセキュリティに関する国際会議The 8th International Conference on Principles of Security and Trust (POST 2019)に採録された。

加えて、一階述語不動点論理による時相仕様検証や循環証明による分離論理のための定理証明など、関連するより一般的なプログラム検証および定理証明についての研究も行った。

現在までの達成度 (区分)
現在までの達成度 (区分)

2: おおむね順調に進展している

理由

研究はおおむね順調に進展している。「研究実績の概要」で述べたとおり、今年度は特にタイミング攻撃に関する研究を行い成果を得た。加えて、定理証明などプログラム検証・プログラム合成のための基盤技術の研究において成果を得た。

今回は、特にサイドチャネル攻撃に関する研究として主にタイミング攻撃に限定して成果をあげたが、研究で得られた知見は電力解析など他のサイドチャネル攻撃にも一般化できると期待される。

今後の研究の推進方策

今年度の研究で得られた知見を元に研究を推進する。まず以下のテーマに取り組む計画である:(1)タイミング攻撃防衛に関する研究の深化、(2)adaptiveなサイドチャネル攻撃に関する研究。具体的に、(1)ではbucketingによるタイミング防衛手法により得られる安全性のより厳密な必要条件・十分条件の導出および他のサイドチャネル攻撃に対する防衛手法への一般化などを目指す。(2)ではadaptiveなサイドチャネル攻撃に関して一般的な議論を行うための枠組みの構築などを目指す。加えて、電力解析などのサイドチャネル攻撃に対して有効な防衛手段であるleakage resilienceについての研究なども行う。

次年度使用額が生じた理由

有償ソフトウェア・サービスの代わりに無償ソフトウェア・サービスの利用および早めの航空券購入などにより次年度使用額が生じた。当該助成金は翌年度分として請求した助成金と合わせて、国内外の学会参加および共同研究者との打ち合わせなど旅費および、研究資料購入など物品費として使用する計画である。

  • 研究成果

    (7件)

すべて 2019 2018

すべて 雑誌論文 (2件) (うち国際共著 2件、 査読あり 2件、 オープンアクセス 2件) 学会発表 (5件) (うち国際学会 4件、 招待講演 2件)

  • [雑誌論文] A Formal Analysis of Timing Channel Security via Bucketing2019

    • 著者名/発表者名
      Terauchi Tachio, Antonopoulos Timos
    • 雑誌名

      In Proceedings of the 8th International Conference on Principles of Security and Trust (POST 2019), Lecture Notes in Computer Science

      巻: 11426 ページ: 29~50

    • DOI

      https://doi.org/10.1007/978-3-030-17138-4_2

    • 査読あり / オープンアクセス / 国際共著
  • [雑誌論文] A Fixpoint Logic and Dependent Effects for Temporal Property Verification2018

    • 著者名/発表者名
      Nanjo Yoji、Unno Hiroshi、Koskinen Eric、Terauchi Tachio
    • 雑誌名

      Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018), ACM

      巻: LICS 2018 ページ: 759~768

    • DOI

      10.1145/3209108.3209204

    • 査読あり / オープンアクセス / 国際共著
  • [学会発表] Solving First-Order Fixpoint Logic for Program Verification2019

    • 著者名/発表者名
      Takashi Nishikawa, Yuki Satake, Yoji Nanjo, Hiroshi Unno, Naoki Kobayashi, Tachio Terauchi, Eric Koskinen
    • 学会等名
      Third Workshop on Mathematical Logic and its Applications (MLA 2019)
    • 国際学会 / 招待講演
  • [学会発表] On Cut-Elimination Theorem in Cyclic-Proof Systems2019

    • 著者名/発表者名
      Koji Nakazawa, Daisuke Kimura, Tachio Terauchi, Hiroshi Unno, Kenji Saotome
    • 学会等名
      Third Workshop on Mathematical Logic and its Applications (MLA 2019)
    • 国際学会
  • [学会発表] Failure of Cut-Elimination in Cyclic Proofs of Separation Logic2019

    • 著者名/発表者名
      Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, Hiroshi Unno
    • 学会等名
      日本ソフトウェア科学会 第21回プログラミングおよびプログラミング言語ワークショップ(PPL2019)
  • [学会発表] On Cut-elimination in Cyclic Proof Systems2019

    • 著者名/発表者名
      Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, Hiroshi Unno
    • 学会等名
      The 4th Workshop on New Ideas and Emerging Results in Programming Languages and Systems (NIER 2018)
    • 国際学会
  • [学会発表] Information Flow Security and its Applications to Side Channel Attack Resilience2018

    • 著者名/発表者名
      Tachio Terauchi
    • 学会等名
      The 4th Franco-Japanese Workshop on Cybersecurity
    • 国際学会 / 招待講演

URL: 

公開日: 2019-12-27  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi