A Hardware Design Language for Timing-Sensitive Information-Flow Security

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.