Formal analysis of macro synchronous micro asychronous pipeline for hardware Trojan detection

F. K. Lodhi, S. R. Hasan, O. Hasan, F. Awwad

Research output: Chapter in Book/Report/Conference proceedingConference contribution

8 Citations (Scopus)

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 paper, 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.

Original languageEnglish
Title of host publication2015 Nordic Circuits and Systems Conference, NORCAS 2015
Subtitle of host publicationNORCHIP and International Symposium on System-on-Chip, SoC 2015
EditorsTor Sverre Lande, Jim Torresen, Oyvind Kallevik Grutle, Ivan Ring Nielsen, Snorre Aunet
PublisherInstitute of Electrical and Electronics Engineers Inc.
ISBN (Electronic)9781467365765
DOIs
Publication statusPublished - Dec 23 2015
Event1st IEEE Nordic Circuits and Systems Conference, NORCAS 2015 - Oslo, Norway
Duration: Oct 26 2015Oct 28 2015

Publication series

Name2015 Nordic Circuits and Systems Conference, NORCAS 2015: NORCHIP and International Symposium on System-on-Chip, SoC 2015

Other

Other1st IEEE Nordic Circuits and Systems Conference, NORCAS 2015
Country/TerritoryNorway
CityOslo
Period10/26/1510/28/15

Keywords

  • Asynchronous
  • Hardware Trojan
  • MSMA
  • Model Checking
  • nuXmv

ASJC Scopus subject areas

  • Hardware and Architecture
  • Electrical and Electronic Engineering

Fingerprint

Dive into the research topics of 'Formal analysis of macro synchronous micro asychronous pipeline for hardware Trojan detection'. Together they form a unique fingerprint.

Cite this