Invited - Specification and modeling for systems-on-chip security verification

Sharad Malik, Pramod Subramanyan

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

9 Scopus citations

Abstract

This paper describes a methodology for system-level security verification of modern Systems-on-Chip (SoC) designs. These designs comprise interacting firmware and hardware modules which makes verification particularly challenging. These challenges relate to (i) specifying security verification properties, and (ii) verifying these properties across firmware and hardware. We address the latter through raising the level of abstraction of the hardware modules to be similar to that of instructions in software/firmware. This abstraction, referred to as an instruction-level abstraction (ILA), plays a similar role to the instruction set architecture (ISA) definition for general purpose processors and enables high-level analysis of SoC firmware. In particular, the ILA can be used instead of the cycle-accurate bit-precise hardware implementation for scalable verification of system-level security properties in SoCs. We introduce techniques to semi-automatically synthesize the ILA using a template abstraction and directed simulations of the SoC hardware. We describe techniques to ensure that the ILA is a correct abstraction of the underlying hardware implementation. We then show how the ILA can be used for SoC security verification by designing a specification language for security properties and an algorithm based on symbolic execution to verify these properties. Our case studies apply ILA-based verification to an example SoC built out of open source components as well as part of a commercial SoC. The methodology discovers several bugs in the hardware implementation, simulators and firmware.

Original languageEnglish (US)
Title of host publicationProceedings of the 53rd Annual Design Automation Conference, DAC 2016
PublisherInstitute of Electrical and Electronics Engineers Inc.
ISBN (Electronic)9781450342360
DOIs
StatePublished - Jun 5 2016
Event53rd Annual ACM IEEE Design Automation Conference, DAC 2016 - Austin, United States
Duration: Jun 5 2016Jun 9 2016

Publication series

NameProceedings - Design Automation Conference
Volume05-09-June-2016
ISSN (Print)0738-100X

Other

Other53rd Annual ACM IEEE Design Automation Conference, DAC 2016
Country/TerritoryUnited States
CityAustin
Period6/5/166/9/16

All Science Journal Classification (ASJC) codes

  • Computer Science Applications
  • Control and Systems Engineering
  • Electrical and Electronic Engineering
  • Modeling and Simulation

Fingerprint

Dive into the research topics of 'Invited - Specification and modeling for systems-on-chip security verification'. Together they form a unique fingerprint.

Cite this