PRECISE Seminar: High-Assurance Multi-Core Processors with Verifiable and Comprehensive Information Flow Control

As computing devices are increasingly consolidated and shared by multiple, potentially distrusting, applications, hardware must be able to provide strong isolation among software entities. For example, automative systems must be able to ensure that safety-critical control modules cannot be affected by passenger entertainment systems. In order to provide high assurance, hardware-level protection mechanisms must be verified to be implemented securely without any unintended bugs or backdoors, and be able to prevent all forms of software-visible information flows including timing channels. This talk will discuss how to design multi-core hardware with verifiable and comprehensive information flow control.

The first part of the talk will discuss how today's multi-core processors can be re-designed to control micro-architectural timing channels and interference among software entities sharing the same hardware. The timing channel protection enables comprehensive control of information flows that are visible to software without physical access. This talk will show the sources of timing channels in today’s multi-core processor and discuss how shared hardware components can be augmented to remove timing dependence. The experimental results suggest that the overhead of timing channel protection can be surprisingly low in modern microprocessors, especially when the number of security domains is small.

The second part of the talk will introduce an extension to today's hardware design language, named SecVerilog, which enables designers to statically analyze information flow at the hardware level and thus to build systems where information channels are verifiably controlled. SecVerilog is Verilog, extended with security type annotations, and comes with rigorous formal assurance: it can prove that hardware enforces timing-sensitive noninterference. Our experiences in designing secure hardware with timing channel protection including pipelined MIPS processors, caches, interconnect, and DRAM controllers suggest that SecVerilog can be used for realistic hardware designs, with low overhead in time, space, and programmer effort.