• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

Program verification and program synthesis for side-channel attack resilience

Research Project

Project/Area Number 18K19787
Research Category

Grant-in-Aid for Challenging Research (Exploratory)

Allocation TypeMulti-year Fund
Review Section Medium-sized Section 60:Information science, computer engineering, and related fields
Research InstitutionWaseda University

Principal Investigator

Terauchi Tachio  早稲田大学, 理工学術院, 教授 (70447150)

Project Period (FY) 2018-06-29 – 2022-03-31
Project Status Completed (Fiscal Year 2021)
Budget Amount *help
¥6,240,000 (Direct Cost: ¥4,800,000、Indirect Cost: ¥1,440,000)
Fiscal Year 2020: ¥2,080,000 (Direct Cost: ¥1,600,000、Indirect Cost: ¥480,000)
Fiscal Year 2019: ¥2,080,000 (Direct Cost: ¥1,600,000、Indirect Cost: ¥480,000)
Fiscal Year 2018: ¥2,080,000 (Direct Cost: ¥1,600,000、Indirect Cost: ¥480,000)
Keywordsサイドチャネル攻撃 / 耐タンパ性 / プログラム検証 / プログラム合成 / 情報セキュリティ
Outline of Final Research Achievements

We have conducted a research on a formal analysis of a timing channel attack mitigation technique called "bucketing". We have obtained results on provable security guarantees achievable with the technique as well as its theoretical limits. We have proposed a game theoretic general framework for proving security of a system against probabilistic and adaptive side channel attacks. We have conducted research on Spectre attacks and ReDoS attacks which are popular timing attacks. Additionally, we have conducted research on more general program verification and automated deduction, including temporal property verification by first-order fixpoint logic solving, relational property verification by predicate constraint solving, type and effect systems for algebraic effects and handlers, and automated deduction for quantified formulas by game solving.

Academic Significance and Societal Importance of the Research Achievements

Bucketingによるタイミング攻撃防衛手法の安全性について初めて形式的な保証を得ることや、確率的かつadaptiveなサイドチャネル攻撃に対する一般的な安全性の議論を可能とするゲーム理論に基づく枠組みを構築するなど、本研究はこれまでのプログラミング言語・形式検証によるセキュリティの研究を大きく飛躍させた。よって、本研究の成果は極めて高い学術的および社会的意義を持つと考える。

Report

(5 results)
  • 2021 Annual Research Report   Final Research Report ( PDF )
  • 2020 Research-status Report
  • 2019 Research-status Report
  • 2018 Research-status Report
  • Research Products

    (16 results)

All 2022 2021 2020 2019 2018

All Journal Article (6 results) (of which Int'l Joint Research: 5 results,  Peer Reviewed: 6 results,  Open Access: 4 results) Presentation (10 results) (of which Int'l Joint Research: 7 results,  Invited: 4 results)

  • [Journal Article] Constraint-Based Relational Verification2021

    • Author(s)
      Unno Hiroshi、Terauchi Tachio、Koskinen Eric
    • Journal Title

      Proceedings of CAV 2021, Springer LNCS

      Volume: 12759 Pages: 742-766

    • DOI

      10.1007/978-3-030-81685-8_35

    • ISBN
      9783030816841, 9783030816858
    • Related Report
      2021 Annual Research Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Journal Article] Failure of Cut-Elimination in Cyclic Proofs of Separation Logic2020

    • Author(s)
      KIMURA Daisuke、NAKAZAWA Koji、TERAUCHI Tachio、UNNO Hiroshi
    • Journal Title

      Computer Software

      Volume: 37 Issue: 1 Pages: 1_39-1_52

    • DOI

      10.11309/jssst.37.1_39

    • NAID

      130007815024

    • ISSN
      0289-6540
    • Year and Date
      2020-01-24
    • Related Report
      2019 Research-status Report
    • Peer Reviewed / Open Access
  • [Journal Article] Bucketing and information flow analysis for provable timing attack mitigation2020

    • Author(s)
      Terauchi Tachio、Antonopoulos Timos
    • Journal Title

      Journal of Computer Security

      Volume: 28 Issue: 6 Pages: 607-634

    • DOI

      10.3233/jcs-191356

    • Related Report
      2020 Research-status Report
    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] A Formal Analysis of Timing Channel Security via Bucketing2019

    • Author(s)
      Terauchi Tachio, Antonopoulos Timos
    • Journal Title

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

      Volume: 11426 Pages: 29-50

    • DOI

      10.1007/978-3-030-17138-4_2

    • ISBN
      9783030171377, 9783030171384
    • Related Report
      2019 Research-status Report 2018 Research-status Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Journal Article] Games for Security Under Adaptive Adversaries2019

    • Author(s)
      Antonopoulos Timos, Terauchi Tachio
    • Journal Title

      In Proceedings of the 32nd IEEE Computer Security Foundations Symposium (CSF 2019)

      Volume: CSF 2019 Pages: 216-229

    • DOI

      10.1109/csf.2019.00022

    • Related Report
      2019 Research-status Report
    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] A Fixpoint Logic and Dependent Effects for Temporal Property Verification2018

    • Author(s)
      Yoji Nanjo, Hiroshi Unno, Eric Koskinen, Tachio Terauchi
    • Journal Title

      Proceedings of LICS 2018

      Volume: 印刷中 Pages: 759-768

    • DOI

      10.1145/3209108.3209204

    • Related Report
      2018 Research-status Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Presentation] 代数的エフェクトハンドラを持つ言語のためのトレースエフェクト2022

    • Author(s)
      川俣楓河、寺内多智弘
    • Organizer
      ソフトウェア科学会 第24回プログラミングおよびプログラミング言語ワークショップ (PPL 2022)
    • Related Report
      2021 Annual Research Report
  • [Presentation] Repairing DoS Vulnerability of Real-World Regexes2022

    • Author(s)
      Nariyoshi Chida and Tachio Terauchi
    • Organizer
      ソフトウェア科学会 第24回プログラミングおよびプログラミング言語ワークショップ (PPL 2022)
    • Related Report
      2021 Annual Research Report
  • [Presentation] Constraint-based Relational Verification2021

    • Author(s)
      Tachio Terauchi
    • Organizer
      Workshop on Hyperproperties: Advances in Theory and Practice (HYPER 2021)
    • Related Report
      2021 Annual Research Report
    • Int'l Joint Research / Invited
  • [Presentation] A Fixpoint Logic and Dependent Effects for Temporal Property Verification2019

    • Author(s)
      Yoji Nanjo, Hiroshi Unno, Eric Koskinen, Tachio Terauchi
    • Organizer
      Dagstuhl Seminar 19371: Deduction Beyond Satisfiability
    • Related Report
      2019 Research-status Report
    • Int'l Joint Research / Invited
  • [Presentation] Inferring Simple Strategies for Efficient Quantified SMT Solving2019

    • Author(s)
      Souta Yamauchi, Tachio Terauchi
    • Organizer
      17th Asian Symposium on Programming Languages and Systems (APLAS 2019)
    • Related Report
      2019 Research-status Report
    • Int'l Joint Research
  • [Presentation] Solving First-Order Fixpoint Logic for Program Verification2019

    • Author(s)
      Takashi Nishikawa, Yuki Satake, Yoji Nanjo, Hiroshi Unno, Naoki Kobayashi, Tachio Terauchi, Eric Koskinen
    • Organizer
      Third Workshop on Mathematical Logic and its Applications (MLA 2019)
    • Related Report
      2018 Research-status Report
    • Int'l Joint Research / Invited
  • [Presentation] On Cut-Elimination Theorem in Cyclic-Proof Systems2019

    • Author(s)
      Koji Nakazawa, Daisuke Kimura, Tachio Terauchi, Hiroshi Unno, Kenji Saotome
    • Organizer
      Third Workshop on Mathematical Logic and its Applications (MLA 2019)
    • Related Report
      2018 Research-status Report
    • Int'l Joint Research
  • [Presentation] Failure of Cut-Elimination in Cyclic Proofs of Separation Logic2019

    • Author(s)
      Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, Hiroshi Unno
    • Organizer
      日本ソフトウェア科学会 第21回プログラミングおよびプログラミング言語ワークショップ(PPL2019)
    • Related Report
      2018 Research-status Report
  • [Presentation] On Cut-elimination in Cyclic Proof Systems2019

    • Author(s)
      Daisuke Kimura, Koji Nakazawa, Tachio Terauchi, Hiroshi Unno
    • Organizer
      The 4th Workshop on New Ideas and Emerging Results in Programming Languages and Systems (NIER 2018)
    • Related Report
      2018 Research-status Report
    • Int'l Joint Research
  • [Presentation] Information Flow Security and its Applications to Side Channel Attack Resilience2018

    • Author(s)
      Tachio Terauchi
    • Organizer
      The 4th Franco-Japanese Workshop on Cybersecurity
    • Related Report
      2018 Research-status Report
    • Int'l Joint Research / Invited

URL: 

Published: 2018-07-25   Modified: 2023-12-25  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi