ガロア体算術に基づく暗号ハードウェアの形式的トロイフリー性検証

• Item type: SIG Technical Reports(1)
• 公開日: 2019-07-16
• タイトル: ガロア体算術に基づく暗号ハードウェアの形式的トロイフリー性検証
• タイトル / 言語: en
• タイトル: A Formal Approach to Verifying Trojan-freeness of Cryptographic Circuits Based on Galois-Field Arithmetic
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 東北大学電気通信研究所
• 著者所属: 東北大学電気通信研究所
• 著者所属: 東北大学電気通信研究所
• 著者所属(英): en
• 著者所属(英): Research Institute of Electrical Communication, Tohoku University
• 著者所属(英): en
• 著者所属(英): Research Institute of Electrical Communication, Tohoku University
• 著者所属(英): en
• 著者所属(英): Research Institute of Electrical Communication, Tohoku University
• 著者名: 伊東, 燦; 上野, 嶺; 本間, 尚文
• 著者名(英): Akira, Ito; Rei, Ueno; Naofumi, Homma
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 本稿では，暗号ハードウェアにハードウェアトロイ (HT: Hardware Trojan) が含まれないことを論理的に保証する HT フリー性検証手法を提案する．提案手法では，暗号ハードウェアの主要な構成要素であるガロア体算術演算回路の機能がガロア体算術式で表されることに着目する．その基本的なアイデアは，検証対象とする暗号ハードウェアのゲートレベル回路記述とガロア体算術式で与えられる設計仕様の形式的等価性判定により，HT による不正な機能改変を検知もしくは機能改変が無いことを検証することである．提案手法では，まず，設計仕様のガロア体算術式をゼロサプレス型二分決定木 (ZDD : Zero-suppressed binary Decision Diagram) 表現によるブール多項式環上の代数方程式に変換する．その上で，検証対象のゲートレベル回路記述から対応するブール多項式環の代数方程式を構築し，設計仕様との同型判定を行うことで，効率的かつ完全な等価性判定を実現する．本稿では，楕円曲線暗号で用いられる実用的なガロア体乗算器を含む様々なビット長のガロア体乗算器および 128 ビット AES ハードウェアデータパスの HT フリー性検証を通して，提案手法が従来と比べて大幅な効率化を達成するとともに従来困難だった実用的な暗号ハードウェアに対しても完全な検証が可能となることを示す．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: This paper proposes a formal method for verifying whether Hardware Trojan (HT) exists or not (i.e.,HT-freeness) in cryptographic hardware. The proposed method focuses on GF arithmetic circuits which are commonly used for a major part of modern cryptographic hardware. Since the functionality of GF arithmetic circuits can be given by a set of GF equations, the proposed method detects the existence of HTs or verifies HT-freeness by checking the equivalence between GF equations (i.e., circuit specification) and flattened gate-level netlist of a target circuit. In the proposed method, we first derive GF equations (i.e., circuit specification) over a representation of Boolean polynomial ring using the zero-suppressed binary decision diagram (ZDD). We then construct the ZDD representation of the target netlist, and finally check whether or not the two ZDDs are isomorphic, which make it possible to perform an efficient and complete HT-freeness verification. In this paper, we demonstrate the highest efficiency of the proposed method through the experimental verification of GF multipliers with various input length including practical ones used in elliptic curve cryptography, and 128-bit AES hardware datapath.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11235941
• 書誌情報: 研究報告コンピュータセキュリティ（CSEC）; 巻 2019-CSEC-86, 号 20, p. 1-6, 発行日 2019-07-16
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 2188-8655
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会