A Formal Approach to Identifying Hardware Trojans in Cryptographic Hardware

研究成果: Conference contribution

抄録

This paper presents a new formal method for detecting and identifying hardware Trojans (HTs) inserted into the datapath of cryptographic hardware based on Galois-field arithmetic such as for the Advanced Encryption Standard and elliptic curve cryptography. To detect HTs, our method first performs equivalence checking between the specifications given as Galois-field polynomials (or the reference circuit of cryptographic hardware) and polynomials representing the input-output relations of a gate-level netlist. Our method exploits zero-suppressed binary decision diagrams for efficient verification. Once an HT is found, the proposed method then detects the trigger condition of the HT using the characteristics of zero-suppressed binary decision diagrams. It also identifies the HT localization using a novel computer algebra method. Our experimental results show that the proposed method can verify netlists and identify HT trigger conditions and locations on a 233-bit multiplier commonly used in elliptic curve cryptography within 1.8 seconds. In addition, we show that if the reference circuit is given, the proposed method can detect a realistic HT inserted into the entire Advanced Encryption Standard hardware, including control logic, in approximately three seconds.

本文言語English
ホスト出版物のタイトルProceedings - 2021 IEEE 51st International Symposium on Multiple-Valued Logic, ISMVL 2021
出版社IEEE Computer Society
ページ154-159
ページ数6
ISBN(電子版)9781728192246
DOI
出版ステータスPublished - 2021 5
イベント51st IEEE International Symposium on Multiple-Valued Logic, ISMVL 2021 - Virtual, Nur-sultan, Kazakhstan
継続期間: 2021 5 252021 5 27

出版物シリーズ

名前Proceedings of The International Symposium on Multiple-Valued Logic
2021-May
ISSN(印刷版)0195-623X

Conference

Conference51st IEEE International Symposium on Multiple-Valued Logic, ISMVL 2021
国/地域Kazakhstan
CityVirtual, Nur-sultan
Period21/5/2521/5/27

ASJC Scopus subject areas

  • コンピュータ サイエンス(全般)
  • 数学 (全般)

フィンガープリント

「A Formal Approach to Identifying Hardware Trojans in Cryptographic Hardware」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル