Formal security verification of concurrent firmware in SoCs using instruction-level abstraction for hardware

Bo Yuan Huang, Sayak Ray, Aarti Gupta, Jason M. Fung, Sharad Malik

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

6 Scopus citations

Abstract

Formal security verification of firmware interacting with hardware in modern Systems-on-Chip (SoCs) is a critical research problem. This faces the following challenges: (1) design complexity and heterogeneity, (2) semantics gaps between software and hardware, (3) concurrency between firmware/hardware and between Intellectual Property Blocks (IPs), and (4) expensive bit-precise reasoning. In this paper, we present a co-verification methodology to address these challenges. We model hardware using the Instruction-Level Abstraction (ILA), capturing firmware-visible behavior at the architecture level. This enables integrating hardware behavior with firmware in each IP into a single thread. The co-verification with multiple firmware across IPs is formulated as a multi-threaded program verification problem, for which we leverage software verification techniques. We also propose an optimization using abstraction to prevent expensive bit-precise reasoning. The evaluation of our methodology on an industry SoC Secure Boot design demonstrates its applicability in SoC security verification.

Original languageEnglish (US)
Title of host publicationProceedings of the 55th Annual Design Automation Conference, DAC 2018
PublisherInstitute of Electrical and Electronics Engineers Inc.
ISBN (Print)9781450357005
DOIs
StatePublished - Jun 24 2018
Event55th Annual Design Automation Conference, DAC 2018 - San Francisco, United States
Duration: Jun 24 2018Jun 29 2018

Publication series

NameProceedings - Design Automation Conference
VolumePart F137710
ISSN (Print)0738-100X

Other

Other55th Annual Design Automation Conference, DAC 2018
CountryUnited States
CitySan Francisco
Period6/24/186/29/18

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 'Formal security verification of concurrent firmware in SoCs using instruction-level abstraction for hardware'. Together they form a unique fingerprint.

  • Cite this

    Huang, B. Y., Ray, S., Gupta, A., Fung, J. M., & Malik, S. (2018). Formal security verification of concurrent firmware in SoCs using instruction-level abstraction for hardware. In Proceedings of the 55th Annual Design Automation Conference, DAC 2018 [a91] (Proceedings - Design Automation Conference; Vol. Part F137710). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1145/3195970.3196055