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

トロイフリー暗号ハードウェアの高水準設計・検証手法の開拓

Research Project

Project/Area Number 20J12887
Research Category

Grant-in-Aid for JSPS Fellows

Allocation TypeSingle-year Grants
Section国内
Review Section Basic Section 60040:Computer system-related
Research InstitutionTohoku University

Principal Investigator

伊東 燦  東北大学, 工学研究科, 特別研究員(DC2)

Project Period (FY) 2020-04-24 – 2022-03-31
Project Status Completed (Fiscal Year 2021)
Budget Amount *help
¥1,700,000 (Direct Cost: ¥1,700,000)
Fiscal Year 2021: ¥800,000 (Direct Cost: ¥800,000)
Fiscal Year 2020: ¥900,000 (Direct Cost: ¥900,000)
Keywordsハードウェアセキュリティ / 暗号 / ハードウェアトロイ / 形式検証 / 暗号ハードウェア / 計算機代数
Outline of Research at the Start

近年,LSIチップに秘密裏に挿入されるバックドアの一種であるハードウェアトロイ(HT)挿入の危険性が指摘されてきている.本研究では,HTが挿入された場合に特にセキュリティ上問題となり得る暗号ハードウェアに焦点を当て,その形式的検証手法の確立を目指す.提案手法では,HTが挿入されていないことを数学的に証明することで検証を行うことから,従来困難と考えられてきたHTの根絶を図ることができる.

Outline of Annual Research Achievements

本年度では,(i)ハードウェアトロイ(HT)のトリガー条件の特定手法,(ii)挿入箇所特定手法の2つの確立を目指して研究を行った.
まず(i)については,HTが挿入された組み合わせ回路と,設計仕様であるガロア体方程式との間で,出力差分を取ることでHTの作動条件を特定する手法を開発した.具体的には,まず,検証対象となる回路の各プライマリ出力について,その論理機能をプライマリ入力変数で書き下した方程式を導出する.この導出過程における多項式表現に,ゼロサプレス型二分決定グラフ(ZDD)を用いることで,高速な多項式導出を可能とする.次に,回路機能を表す多項式と,設計仕様となるガロア体方程式の間で差分を取ることで,HTの機能を表現した方程式を導出する.最後に,この差分の方程式について,充足可能条件を導くことで,HTの動作条件を特定する.
次に,(ii)については,挿入されるHTが,特定の入力候補でのみ動作することに注目し,それをうまく活用することでHTにあたる論理ゲートを絞り込む手法を提案した.提案手法では,まず回路上のすべての論理ゲートについて,その機能をガロア体方程式として導出する.次に,ガロア体方程式の次数が,活性化確率の負の対数に比例するという特徴を利用して,HTに対応する論理ゲートを絞り込む.提案手法では,論理ゲートの充足条件の数を直接求めるのではなく,ガロア体方程式の次数に着目することで,高速にHTを絞り込むことが可能である.
上記の(i)と(ii)の有効性を確認するために,楕円曲線暗号向けのガロア体乗算器と,AESについてHT検知実験を行った.前者については,従来手法や形式検証ツールであるSynopsys Formalityよりも短い時間で,HTが検知可能なことを示した.また,AESについても,約3秒でHTの動作条件および挿入箇所特定が可能なことを示した.

Research Progress Status

令和3年度が最終年度であるため、記入しない。

Strategy for Future Research Activity

令和3年度が最終年度であるため、記入しない。

Report

(2 results)
  • 2021 Annual Research Report
  • 2020 Annual Research Report
  • Research Products

    (8 results)

All 2022 2021 2020

All Journal Article (3 results) (of which Peer Reviewed: 3 results,  Open Access: 3 results) Presentation (4 results) (of which Int'l Joint Research: 2 results) Funded Workshop (1 results)

  • [Journal Article] Efficient Formal Verification of Galois-Field Arithmetic Circuits Using ZDD Representation of Boolean Polynomials2022

    • Author(s)
      Ito Akira、Ueno Rei、Homma Naofumi
    • Journal Title

      IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems

      Volume: 41 Issue: 3 Pages: 794-798

    • DOI

      10.1109/tcad.2021.3059924

    • Related Report
      2021 Annual Research Report 2020 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] An Algebraic Approach to Verifying Galois-Field Arithmetic Circuits with Multiple-Valued Characteristics2021

    • Author(s)
      ITO Akira、UENO Rei、HOMMA Naofumi
    • Journal Title

      IEICE Transactions on Information and Systems

      Volume: E104.D Issue: 8 Pages: 1083-1091

    • DOI

      10.1587/transinf.2020LOP0004

    • NAID

      130008070385

    • ISSN
      0916-8532, 1745-1361
    • Year and Date
      2021-08-01
    • Related Report
      2021 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] Imbalanced Data Problems in Deep Learning-Based Side-Channel Attacks: Analysis and Solution2021

    • Author(s)
      Ito Akira、Saito Kotaro、Ueno Rei、Homma Naofumi
    • Journal Title

      IEEE Transactions on Information Forensics and Security

      Volume: 16 Pages: 3790-3802

    • DOI

      10.1109/tifs.2021.3092050

    • Related Report
      2021 Annual Research Report
    • Peer Reviewed / Open Access
  • [Presentation] A Formal Approach to Identifying Hardware Trojans in Cryptographic Hardware2021

    • Author(s)
      Akira Ito
    • Organizer
      IEEE 51th International Symposium on Multiple-Valued Logic (ISMVL)
    • Related Report
      2021 Annual Research Report
    • Int'l Joint Research
  • [Presentation] Effective Formal Verification for Galois-field Arithmetic Circuits with Multiple-Valued Characteristics2020

    • Author(s)
      Akira Ito, Rei Ueno, and Naofumi Homma
    • Organizer
      IEEE 50th International Symposium on Multiple-Valued Logic
    • Related Report
      2020 Annual Research Report
    • Int'l Joint Research
  • [Presentation] 暗号ハードウェアのネットリストに対するハードウェアトロイ検知手法2020

    • Author(s)
      伊東燦, 上野嶺, 本間尚文
    • Organizer
      ハードウェアセキュリティ研究会
    • Related Report
      2020 Annual Research Report
  • [Presentation] 決定グラフ表現に基づくハードウェアトロイ検知手法2020

    • Author(s)
      伊東 燦, 上野 嶺, 本間 尚文
    • Organizer
      第43回多値論理フォーラム
    • Related Report
      2020 Annual Research Report
  • [Funded Workshop] IEEE 50th International Symposium on Multiple-Valued Logic2020

    • Related Report
      2020 Annual Research Report

URL: 

Published: 2020-07-07   Modified: 2024-03-26  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi