TY - GEN
T1 - Formal security verification of concurrent firmware in SoCs using instruction-level abstraction for hardware
AU - Huang, Bo Yuan
AU - Ray, Sayak
AU - Gupta, Aarti
AU - Fung, Jason M.
AU - Malik, Sharad
N1 - Funding Information:
∗This work was supported in part by Semiconductor Research Corporation (SRC). It was performed during the first author’s internship at Intel Corp.
Publisher Copyright:
© 2018 Association for Computing Machinery.
PY - 2018/6/24
Y1 - 2018/6/24
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85053676983&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85053676983&partnerID=8YFLogxK
U2 - 10.1145/3195970.3196055
DO - 10.1145/3195970.3196055
M3 - Conference contribution
AN - SCOPUS:85053676983
SN - 9781450357005
T3 - Proceedings - Design Automation Conference
BT - Proceedings of the 55th Annual Design Automation Conference, DAC 2018
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 55th Annual Design Automation Conference, DAC 2018
Y2 - 24 June 2018 through 29 June 2018
ER -