Imran Hafeez Abbasi, Faiq Khalid Lodhi , Osman Hasan and Awais Mehmood Kamboh
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 this work, we propose a framework to formally model and analyze the gate-level side channel parameters, i.e., dynamic power and delay, for Hardware Trojan detection. We used the nuXmv model checker for the formal modeling and analysis of integrated circuits due to its inherent capability of handling real numbers and support of scalable SMT-based bounded model checking. The experimental results show that the proposed methodology is able to detect the intrusions by analyzing the failure of the specified linear temporal logic (LTL) properties, which are subsequently rendered into behavioral traces, indicating the potential attack paths in integrated circuits.