TY - GEN
T1 - Invited - Specification and modeling for systems-on-chip security verification
AU - Malik, Sharad
AU - Subramanyan, Pramod
N1 - Publisher Copyright:
© 2016 ACM.
PY - 2016/6/5
Y1 - 2016/6/5
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84977103546&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84977103546&partnerID=8YFLogxK
U2 - 10.1145/2897937.2911991
DO - 10.1145/2897937.2911991
M3 - Conference contribution
AN - SCOPUS:84977103546
T3 - Proceedings - Design Automation Conference
BT - Proceedings of the 53rd Annual Design Automation Conference, DAC 2016
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 53rd Annual ACM IEEE Design Automation Conference, DAC 2016
Y2 - 5 June 2016 through 9 June 2016
ER -