セキュリティハードウェアの形式的設計・検証理論の深化と展開

• Project/Area Number: 21H04867
• Research Category: Grant-in-Aid for Scientific Research (A)
• Allocation Type: Single-year Grants
• Section: 一般
• Review Section: Medium-sized Section 60:Information science, computer engineering, and related fields
• Research Institution: Tohoku University
• Principal Investigator: 本間 尚文 東北大学, 電気通信研究所, 教授 (00343062)
• Co-Investigator(Kenkyū-buntansha): 上野 嶺 京都大学, 情報学研究科, 准教授 (80826165)
• Project Period (FY): 2021-04-05 – 2026-03-31
• Project Status: Granted (Fiscal Year 2024)
• Budget Amount: ¥41,080,000 (Direct Cost: ¥31,600,000、Indirect Cost: ¥9,480,000); Fiscal Year 2025: ¥13,260,000 (Direct Cost: ¥10,200,000、Indirect Cost: ¥3,060,000); Fiscal Year 2024: ¥8,580,000 (Direct Cost: ¥6,600,000、Indirect Cost: ¥1,980,000); Fiscal Year 2023: ¥8,190,000 (Direct Cost: ¥6,300,000、Indirect Cost: ¥1,890,000); Fiscal Year 2022: ¥5,460,000 (Direct Cost: ¥4,200,000、Indirect Cost: ¥1,260,000); Fiscal Year 2021: ¥5,590,000 (Direct Cost: ¥4,300,000、Indirect Cost: ¥1,290,000)
• Keywords: 計算機システム / 情報セキュリティ / ハードウェアセキュリティ

Outline of Research at the Start

本研究は，暗号や誤り訂正等の機能を搭載するセキュリティハードウェアの形式的設計・検証技術の確立を目指す．まず，非冗長・冗長ガロア体算術が混在する多様なガロア体算術演算回路の統一的な形式的設計手法を開発し，その回路表現を完全かつ高速に検証する計算機代数に基づく形式的検証手法を開発する．その上で，次世代暗号や物理複製困難関数等を実行する先端的なセキュリティハードウェアを対象として，その有効性を実証する．

Outline of Annual Research Achievements

前年度までに開発したHDL記述の等価性判定を可能とする形式的検証手法を開発するとともに，暗号ハードウェアに適用し，その有効性評価を実施した．開発手法では，まず，検証対象となる回路仕様と回路記述をそれぞれ多項式もしくは多項式の集合と見なして，その正規形であるグレブナー基底を導出する．ここで，特殊な変数順序（逆トポロジー項順序）をとることにより得られる多項式が自ずとグレブナー基底になることが開発手法の特長となる．本年度は，その特長を数学的に証明した．これにより，同手法を様々な回路に適用する方向性が定まった．さらに多項式をZDD（Zero-suppressed Decision Diagram）に変換することで高次の多項式であってもコンパクトに表現できる効果を実用的な暗号ハードウェアへの適用を通して確認した． その結果，ガロア体演算機能の場合，指数的に表現サイズを削減できることを示した．また，結果として得られるZDD集合はグレブナー基底と等価なことが数学的に保証できるため，別途グレブナー基底を導出する膨大な計算を省略できることも応用を通して確認できた．特に，本年度は，これまで規模の面で困難だった先端的なセキュリティハードウェアの例として，現在世界で最も利用されている暗号AESへの適用を行った．AESは，その暗号化・復号処理全体がガロア体上の演算として記述されるため，開発した手法を用いて組み合わせ回路部分のデータパス全体の設計・検証を実施した．さらに，本年度は，消費電力面で優れたハードウェアアーキテクチャへの適用も検討し，その可能性を実験的に示した．

Current Status of Research Progress

2: Research has progressed on the whole more than it was originally planned.

Reason

当初予定していた成果が得られており，今後の計画に対する道筋も見えている．具体的には，
前年度までに開発したHDL記述の等価性判定を可能とする形式的検証手法を開発するとともに，暗号ハードウェアに適用し，その有効性評価を実施した．開発手法では，まず，検証対象となる回路仕様と回路記述をそれぞれ多項式もしくは多項式の集合と見なして，その正規形であるグレブナー基底を導出する．ここで，特殊な変数順序（逆トポロジー項順序）をとることにより得られる多項式が自ずとグレブナー基底になることが開発手法の特長となる．本年度は，その特長を数学的にも証明した．さらに多項式をZDD（Zero-suppressed Decision Diagram）に変換することで高次の多項式であってもコンパクトに表現できることを暗号ハードウェアへの適用を通して確認した． また，結果として得られるZDD集合はグレブナー基底と等価なことが数学的に保証できるため，別途グレブナー基底を導出する膨大な計算を省略できることも応用を通して確認できた．特に，本年度は，これまで規模の面で困難だった先端的なセキュリティハードウェアの例として，現在世界で最も利用されている暗号AESへの適用を行った．AESは，その暗号化・復号処理全体がガロア体上の演算として記述されるため，開発した手法を用いて組み合わせ回路部分のデータパス全体の設計・検証を実施した．さらに，本年度は，消費電力面で優れたハードウェアアーキテクチャへの適用も検討し，その可能性を実験的に示した．研究を進めるにつれて新たな課題・関連する課題も出現しているが，新たな課題に対しては定式化・実験方法等の変更で対応可能であり，当初研究計画を変更するほどではない．以上から，「おおむね順調に進展している」と自己評価した．

Strategy for Future Research Activity

上述の通り現時点では研究を遂行する上での問題点はないため，今後も当初研究計画に沿って推進していく．すなわち，これまでに開発した形式的検証手法をさらに高度な暗号ハードウェアに適用し，その有効性評価を実施する．特に，消費電力面で優れたハードウェアアーキテクチャへの適用に加えて，物理攻撃耐性を有するセキュアアーキテクチャを対象に開発手法の有効性を実証する．物理攻撃耐性を有するハードウェアへの適用では，実際に物理攻撃耐性評価実験も並行して実施し，その実用性を明らかにする．さらに，回路にバグやハードウェアトロイがある場合を想定し，それを同定する手法へと開発手法を発展させる．ここでは，等価性検証の結果として得られるZDDの残差からその作動条件および存在箇所を同定する手法を開発する．

Research Products

• [Int'l Joint Research] Nanyang Technological University(シンガポール)
• [Int'l Joint Research] Telecom Paris(フランス)
• [Int'l Joint Research] Nanyang Technological University(シンガポール)
• [Int'l Joint Research] Telecom Paris(フランス)
• [Int'l Joint Research] Nanyang Technological University(シンガポール)
• [Int'l Joint Research] Telecom Paris(フランス)
• [Journal Article] Efficient DFA-Resistant AES Hardware Based on Concurrent Fault Detection Scheme (2023)
  • Author(s): Ueno Rei、Yagyu Yusuke、Homma Naofumi
  • Journal Title: 2023 IEEE 53rd International Symposium on Multiple-Valued Logic Volume: 1 Pages: 196-201
  • DOI: 10.1109/ismvl57333.2023.00045
  • Peer Reviewed
• [Journal Article] Multiple-Valued Plaintext-Checking Side-Channel Attacks on Post-Quantum KEMs (2023)
  • Author(s): Tanaka Yutaro、Ueno Rei、Xagawa Keita、Ito Akira、Takahashi Junko、Homma Naofumi
  • Journal Title: IACR Transactions on Cryptographic Hardware and Embedded Systems Volume: 4 Pages: 473-503
  • DOI: 10.46586/tches.v2023.i3.473-503
  • Peer Reviewed / Open Access
• [Journal Article] Side-Channel Analysis Against SecOC-Compliant AES-CMAC (2023)
  • Author(s): Ebina Katsumi、Ueno Rei、Homma Naofumi
  • Journal Title: IEEE Transactions on Circuits and Systems II: Express Briefs Volume: 70 Issue: 10 Pages: 3772-3776
  • DOI: 10.1109/tcsii.2023.3288278
  • Peer Reviewed / Open Access
• [Journal Article] Fallen Sanctuary: A Higher-Order and Leakage-Resilient Rekeying Scheme (2023)
  • Author(s): Ueno Rei、Homma Naofumi、Inoue Akiko、Minematsu Kazuhiko
  • Journal Title: IACR Transactions on Cryptographic Hardware and Embedded Systems Volume: 2024 Issue: 1 Pages: 264-308
  • DOI: 10.46586/tches.v2024.i1.264-308
  • Peer Reviewed / Open Access
• [Journal Article] High-Speed Hardware Architecture for Post-Quantum Diffie?Hellman Key Exchange Based on Residue Number System (2022)
  • Author(s): Ueno Rei、Homma Naofumi
  • Journal Title: Proceedings on IEEE International Symposium on Circuits and Systems Volume: - Pages: 2107-2111
  • DOI: 10.1109/iscas48785.2022.9937804
  • Peer Reviewed / Open Access
• [Journal Article] AES S-Box Hardware With Efficiency Improvement Based on Linear Mapping Optimization (2022)
  • Author(s): Nakashima Ayano、Ueno Rei、Homma Naofumi
  • Journal Title: IEEE Transactions on Circuits and Systems II: Express Briefs Volume: 69 Issue: 10 Pages: 3978-3982
  • DOI: 10.1109/tcsii.2022.3185632
  • Peer Reviewed / Open Access
• [Journal Article] Efficient Modular Polynomial Multiplier for NTT Accelerator of Crystals-Kyber (2022)
  • Author(s): Itabashi Yuma、Ueno Rei、Homma Naofumi
  • Journal Title: Proceedings on Euromicro Conference on Digital System Design Volume: - Pages: 528-533
  • DOI: 10.1109/dsd57027.2022.00076
  • Peer Reviewed / Open Access
• [Journal Article] Efficient Formal Verification of Galois-Field Arithmetic Circuits Using ZDD Representation of Boolean Polynomials (2022)
  • 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
  • Peer Reviewed / Open Access
• [Journal Article] An Algebraic Approach to Verifying Galois-Field Arithmetic Circuits with Multiple-Valued Characteristics (2021)
  • 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
  • Peer Reviewed / Open Access
• [Journal Article] A Systematic Design Methodology of Formally-Proven Side-Channel-Resistant Cryptographic Hardware (2021)
  • Author(s): Ueno Rei、Homma Naofumi、Morioka Sumio、Aoki Takafumi
  • Journal Title: IEEE Design & Test Volume: － Issue: 3 Pages: 1-1
  • DOI: 10.1109/mdat.2021.3063337
  • Peer Reviewed / Open Access
• [Journal Article] A Formal Approach to Identifying Hardware Trojans in Cryptographic Hardware (2021)
  • Author(s): Ito Akira、Ueno Rei、Homma Naofumi
  • Journal Title: IEEE 51th International Symposium on Multiple-Valued Logic Volume: 1 Pages: 154-159
  • DOI: 10.1109/ismvl51352.2021.00034
  • Peer Reviewed
• [Presentation] GF(2m)上の算術演算順序回路の計算機代数に基づく形式検証に関する検討 (2024)
  • Author(s): 迫田一歩, 植村泰佳，本間尚文
  • Organizer: 電子情報通信学会ハードウェアセキュリティ研究会
• [Presentation] Triviumのアンロールド実装に対するサイドチャネル攻撃の検討 (2023)
  • Author(s): 小林蒼一朗, 上野嶺, 藤堂洋介, 本間尚文
  • Organizer: 電子情報通信学会情報セキュリティ研究会
• [Presentation] ASCONへのサイドチャネル攻撃における選択関数に関する検討 (2023)
  • Author(s): 岩佐大将，上野嶺，福島和英，本間尚文
  • Organizer: 電子情報通信学会情報セキュリティ研究会
• [Presentation] アンロールド実装されたブロック暗号に対するサイドチャネル攻撃と差分解読の関係性の検討 (2023)
  • Author(s): 東哲平, 上野嶺, 本間尚文
  • Organizer: 電子情報通信学会情報セキュリティ研究会
• [Presentation] 耐量子計算機暗号ハードウェア設計の基礎 (2023)
  • Author(s): 本間尚文
  • Organizer: 応用物理学会超集積エレクトロニクス産学連携委員会「夏の学校」
  • Invited
• [Presentation] AI Security from Hardware Perspective (2023)
  • Author(s): Naofumi Homma
  • Organizer: 6th Tohoku Uni-NTU Symposium on Interdisciplinary AI and Human Studies
  • Int'l Joint Research / Invited
• [Presentation] ハードウェアトロイフリーを実現するLSIシステム設計技術 (2023)
  • Author(s): 本間尚文
  • Organizer: 電子情報通信学会総合大会
  • Invited
• [Presentation] 確率的秘匿演算ハードウェアの設計とプロトタイプ評価, (2022)
  • Author(s): 田村佑樹
  • Organizer: 電子情報通信学会ハードウェアセキュリティ研究会
• [Presentation] 耐量子計算機暗号の耐タンパー実装技術の最新動向 (2022)
  • Author(s): 本間尚文
  • Organizer: Security Days 2022 Fall
  • Invited
• [Presentation] Post-Quantum Cryptography - The Way Forward (2022)
  • Author(s): Naofumi Homma
  • Organizer: Asian HOST 2022
  • Int'l Joint Research / Invited
• [Presentation] アンロールド実装されたAESハードウェア特有のサイドチャネル情報漏洩の評価 (2022)
  • Author(s): 中嶋彩乃
  • Organizer: 電子情報通信学会ハードウェア研究会
• [Presentation] 耐量子計算機暗号ソフトウェア・ハードウェアの耐タンパー実装技術の最新動向 (2022)
  • Author(s): 本間尚文
  • Organizer: Security Days 2022 Spring
  • Invited
• [Presentation] 耐量子計算機暗号に対するサイドチャネル攻撃 (2022)
  • Author(s): 本間尚文
  • Organizer: 電子情報通信学会総合大会
  • Invited
• [Presentation] 剰余数系を用いた同種写像暗号の高速ハードウェア実装 (2021)
  • Author(s): 上野 嶺
  • Organizer: 電子情報通信学会ハードウェアセキュリティ研究会
• [Presentation] 格子暗号向け数論変換ハードウェアの設計 (2021)
  • Author(s): 板橋由磨
  • Organizer: 第44回多値論理フォーラム
• [Presentation] 格子暗号向けKリダクションに基づく数論変換ハードウェアの検討 (2021)
  • Author(s): 板橋由磨
  • Organizer: 電子情報通信学会ハードウェアセキュリティ研究会
• [Presentation] Secure Cryptographic Circuit Design against Side-Channel Attacks (2021)
  • Author(s): Naofumi Homma
  • Organizer: IEEE 47th European Solid-State Circuits Conference
  • Int'l Joint Research / Invited
• [Remarks] 東北大学電気通信研究所環境調和型セキュア情報システム研究分野
  • URL: http://www.ecsis.riec.tohoku.ac.jp/