Hardware Trojan Detection using Model Checking

The enhancements in functionality, performance, and complexity in modern electronics systems have ensued the involvement of various entities, around the globe, in different phases of integrated circuit (IC) manufacturing. This environment has exposed the ICs to malicious intrusions also referred as Hardware Trojans (HTs). The detection of malicious intrusions in ICs with exhaustive simulations and testing is computationally intensive, and it takes substantial effort and time for all-encompassing verification. In order to overcome this limitation, in these work, we propose a framework to formally model and analyze the functional and gate-level side channel parameters, i.e., dynamic power and delay, for Hardware Trojan detection.

1. Formal Verification of Gate-Level Multiple Side Channel Parameters to detect Hardware Trojans
2. Formal Analysis of Macro Synchronous Micro Asychronous Pipeline for Hardware Trojan Detection

Publications

1. I. Abbasi, F. K. Lodhi, A. Kamboh, O. Hasan, “Formal Verification of Gate-Level Multiple Side Channel Parameters to detect Hardware Trojans“, Fifth International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2016), Tokyo, Japan, To Appear.

2. F. K. Lodhi, O. Hasan, S. R. Hasan and F. Awwad,”Formal Analysis of Macro Synchronous Micro Asychronous Pipeline for Hardware Trojan Detection, ” in Nordic Circuits and Systems Conference (NORCAS 2015): NORCHIP & International Symposium on System-on-Chip (SoC), Oct. 2015, pp. 1 – 4.