A Formal Approach to Identifying Hardware Trojans in Cryptographic Hardware

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish
Title of host publicationProceedings - 2021 IEEE 51st International Symposium on Multiple-Valued Logic, ISMVL 2021
PublisherIEEE Computer Society
Pages154-159
Number of pages6
ISBN (Electronic)9781728192246
DOIs
Publication statusPublished - 2021 May
Event51st IEEE International Symposium on Multiple-Valued Logic, ISMVL 2021 - Virtual, Nur-sultan, Kazakhstan
Duration: 2021 May 252021 May 27

Publication series

NameProceedings of The International Symposium on Multiple-Valued Logic
Volume2021-May
ISSN (Print)0195-623X

Conference

Conference51st IEEE International Symposium on Multiple-Valued Logic, ISMVL 2021
Country/TerritoryKazakhstan
CityVirtual, Nur-sultan
Period21/5/2521/5/27

Keywords

  • cryptographic hardware
  • decision diagrams
  • formal methods
  • Hardware Trojan detections

ASJC Scopus subject areas

  • Computer Science(all)
  • Mathematics(all)

Fingerprint

Dive into the research topics of 'A Formal Approach to Identifying Hardware Trojans in Cryptographic Hardware'. Together they form a unique fingerprint.

Cite this