Information Flow Analysis For Security Verification Of Hardware Design

Abstract

We have witnessed the widespread adoption of computers, tablets and smartphones in recent years. When people in the modern society become more and more dependent on these devices, it is essential and necessary to protect user's information security and privacy while guaranteeing the high performance of these devices at the same time. There has been lots of researching on software layer to prevent malwares and viruses from affecting PCs, tablets and smartphones. On the other hand, with software security tools and network vulnerabilities being constantly targeted, hardware-based security solutions are growing in importance. Currently, the main concern of hardware security lies on how to design secure hardware, like ARM's TrustZone, and Intels Trusted Execution Technology(TXT). In this thesis, we explore challenges and opportunities in how to verify the security of hardware designs. We choose TrustZone architecture as the security model, and build a multicore prototype to support TrustZone features. We encode TrustZone architecture with information flow, and take advantage of SecVerilog, a tool for security check, to verify implemented TrustZone prototype. According to evaluation results, we also summarize the limitations of SecVerilog.