Publications in Scientific Journals:

F. Khalid, S. R. Hasan, O. Hasan, F. Awwad:
"Runtime Hardware Trojan Monitors Through Modeling Burst Mode Communication Using Formal Verification";
Integration the VLSI journal, 61 (2018), C; 62 - 76.

English abstract:
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).

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

"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)

Created from the Publication Database of the Vienna University of Technology.