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

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).