A Hardware Design Language for Timing-Sensitive Information-Flow Security
Danfeng Zhang*, Yao Wang†, G. Edward Suh†, and Andrew C. Myers*
*Department of Computer Science, †Department of Electrical and Computer Engineering, Cornell University
March 15–18, Istanbul, Turkey
Information security can be compromised by leakage via low-level hardware features. For example, hardware features can create timing channels such as cache probing attacks, which constitute a real security risk. We introduce a hardware design language, SecVerilog, which makes it possible to statically analyze information flow at the hardware level and thus to build systems in which timing channels and other information channels are verifiably controlled. SecVerilog is Verilog, extended with expressive type annotations that enable precise reasoning about information flow. SecVerilog also comes with rigorous formal assurance: we prove that it enforces timing-sensitive noninterference, ensuring secure information flow. By building a secure MIPS processor and its caches, we demonstrate that SecVerilog makes it possible to build complex hardware designs with verified security, yet with low overhead in time, space, and programmer effort.