Scalable Verification of Security Properties in SoCs
Contemporary SoCs pose challenges in verifying security properties due to the combination of hardware and firmware components. This work discusses the complexities of verifying SoCs, the construction of Instruction-Level Abstraction (ILA), and the synthesis of ILA using advanced techniques. Security verification is particularly challenging, focusing on confidentiality and integrity aspects. Information flow properties play a crucial role in specifying security requirements for SoCs.
- SoCs
- Security Verification
- Instruction-Level Abstraction
- Information Flow Properties
- Scalable Verification
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
Specification and Scalable Verification of Security Properties in Contemporary SoCs Pramod Subramanyan This work was supported in part by CFAR, one of the six SRC STARTnet centers, sponsored by MARCO and DARPA
Birds Eye View of an SoC CPU GPU Camera Touch Flash Microcontroller On-chip Interconnect Memory MMU+ DRAM DMA WiFi/3G SCIP HW accelerators SoC functionality is implemented by a combination of hardware and firmware NoC interface 2
SoC Verification is Challenging CPU GPU Camera Touch Flash On-chip Interconnect MMU+ DRAM Complete verification is not scalable DMA WiFi/3G SCIP Separate verification misses bugs! FW 3
Constructing an ILA Insight: Treat MMIO reads/writes as part of an extended ISA aka ILA ; start AES state machine MOV ACC, #01 MOV DPTR, #0xFF00 MOVX @DPTR, ACC IDLE READ ; poll for completion wait_finish: MOV MOVX ACC, @DPTR CMPI ACC, #00 JNZ WRITE ENC DPTR, #0xFF01 Instruction-Level Model of HW accelerators wait_finish Instruction-Level Model of c ISA Instruction-Level Abstraction (ILA) of SoC 4
Synthesizing an ILA [FMCAD 15] It s too hard to manually construct an ILA so synthesize it instead! FW verification Template abstraction Synthesis Algorithm Instruction-Level Abstraction Golden Model Model Checker Simulator RTL Refinement Relations Bugs/counter examples 5
Security Verification is Harder! Confidentiality: HW/FW secrets must not leak to untrusted entities secret SoC Integrity: Untrusted entities must not influence sensitive registers reg Specifying these in LTL is hard! Not predicates of state, instead these properties refer to information flow! 6
Specifying Information Flow Properties Information flow property specifies that src cannot influence dst src dst Specified on an augmented ILA Properties High-level system state such as user/su mode, current thread and VM ids, and son Convert events such as user/su state-transitions into state variables HW model HW model FW model aux stat e Augmented System Model FW model Original System Model 7
Proving Information Flow Properties In the security community: static and dynamic taint analysis Can different values at the source result in different values at the destination? T src1 dst1 inp T src2 dst2 Can we do better with a taint+CEGAR hybrid? 8
HW/FW Security Concerns are an Important and Exciting Research Area http://www.wired.com/2015/07/hackers-remotely-kill-jeep-highway/ Come to the poster to talk more! 9
