Runtime hardware Trojan monitors through modeling burst mode communication using formal verification

Faiq Khalid, Syed Rafay Hasan, Osman Hasan, Falah Awwad

Research output: Contribution to journalArticlepeer-review

20 Citations (Scopus)


Globalization trends in integrated circuit (IC) design using deep sub-micron (DSM) technologies are leading to increased vulnerability against malicious intrusions. Various techniques have been proposed to detect such threats during design or testing phases of ICs. However, due to infinitely many possibilities of Trojans, there exists a possibility that some of these intrusions go undetected. Therefore, runtime Trojan detection techniques are needed to detect the Trojans for complete operation lifetime as a last line of defense. In this paper, we proposed a generic methodology, which leverages the burst mode communication protocol, to detect the intrusions during runtime. Our methodology has three phases: 1) behavioral modeling of design specifications along with its verification using linear temporal logic (LTL) in the model checker. 2) Counterexamples generated in phase 1 are used to insert run-time monitors at vulnerable paths. 3) Embed run-time monitors into the system and validate it. Unlike the other state-of-the-art techniques, the proposed methodology can be easily used to design the runtime monitoring setup without having netlist information of IP modules. We validated our approach by applying it on the AES Trojan benchmarks that utilize intermodule interface to communicate with other modules in the system on chip (SoC).

Original languageEnglish
Pages (from-to)62-76
Number of pages15
Publication statusPublished - Mar 2018


  • Burst mode communication
  • Formal verification
  • Hardware Trojans
  • Model checking
  • Network on Chip (NoC)
  • Runtime monitors

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture
  • Electrical and Electronic Engineering


Dive into the research topics of 'Runtime hardware Trojan monitors through modeling burst mode communication using formal verification'. Together they form a unique fingerprint.

Cite this