Visible to the public Formal Security Verification of Concurrent Firmware in SoCs Using Instruction-Level Abstraction for Hardware*

TitleFormal Security Verification of Concurrent Firmware in SoCs Using Instruction-Level Abstraction for Hardware*
Publication TypeConference Paper
Year of Publication2018
AuthorsHuang, Bo-Yuan, Ray, Sayak, Gupta, Aarti, Fung, Jason M., Malik, Sharad
Conference Name2018 55th ACM/ESDA/IEEE Design Automation Conference (DAC)
Date PublishedJune 2018
ISBN Number978-1-5386-4114-9
KeywordsAccess Control, architecture level, bit-precise reasoning, Cognition, composability, Concurrency, concurrency (computers), concurrent firmware, cyber-physical system, Cyber-physical systems, firmware, firmware-visible behavior, formal security verification, Frequency modulation, Hardware, Instruction-Level Abstraction, intellectual property blocks, intellectual property security, Metrics, microprocessor chips, Microprogramming, multi-threading, multithreaded program verification problem, Predictive Metrics, program verification, pubcrawl, resilience, Resiliency, Secure Boot design, security of data, SoC security verification, software verification techniques, system-on-chip, Systems-on-Chip

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.

Citation Keyhuang_formal_2018