Formal Analysis of MSMA Pipeline for Hardware Trojan Detection

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

Abstract

Globalization trends in integrated circuit (IC) design using deep submicron (DSM) technologies are leading to increased vulnerability of IC against malicious intrusions. These malicious intrusions are referred to hardware Trojans. One way to address this threat is to utilize unique electrical signatures of ICs, and any deviation from this signature helps in detecting the potential attack paths. Recently we proposed hybrid macro synchronous micro asynchronous (MSMA) pipeline technique while utilizing, non-conventional, asynchronous circuits to generate timing signature. However, traditionally generating these timing signatures with environmental uncertainties require extensive simulations. It is known to the engineering community that computer simulations have its limitations due to the associated heavy computational requirements. In this project, as a more accurate alternative, we propose a framework to detect the vulnerable paths in the MSMA pipeline for hardware Trojan detection using formal verification methods. In particular, the paper presents a formal model of the MSMA pipeline and its verification results for both functional and timing properties.

nad

Low Power Soft Error Tolerant Macro Synchronous Micro Asynchronous (MSMA) Pipeline

nad

Test vector insertion to obtain timing signature in MSMA

 

Formal Analysis

nad

Potential Attack Path when Asynchronous Registers are intruded

nad

FSM of Hardware Trojan Detetion in MSMA

 

nad

Function and Timing Analysis

Publications

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