Timing-Safe Hardware Level Information Flow Control

Abstract

Developing secure processors has become increasingly important. Recent advancements in commercial security architectures such as Intel SGX have garnered much attention. The promise of these architectures is compelling; because the root of trust lies in hardware, the system it protects remains secure even if low-level software such as the operating system is compromised. Unfortunately, hardware is itself complex and error-prone – software-exploitable vulnerabilities in SGX have already been found, and bugs in hardware have a long history of causing security vulnerabilities. Even if hardware is correct in the conventional sense that it conforms to a specification, security is not assured. Processors still leak secrets through microarchitectural timing channels, and virtually every hardware feature that improves performance has been exploited to leak secrets. Information flow security is a promising approach for verifying hardware systems. Information flow tracks and constrains the movement of data throughout a system ensuring that confidentiality and integrity are not violated. Information flow control can be enforced by a type system embedded in a secure hardware description language (HDL) with which the hardware is described. With this approach, the HDL includes features for describing security policies. The type system of the HDL then statically proves at design-time that the security policies are always enforced. This thesis enables future hardware designs to provide strong assurance through information flow control. This is achieved through two major thrusts of research: 1) developing a practical, expressive hardware description language for enforcing information flow control in hardware designs and 2) designing secure hardware that is suitable for information flow verification. In particular, this thesis describes a number of contributions to secure HDLs that were implemented as extensions to a secure HDL called SecVerilog. It also describes ChiselFlow, a variant of the HDL, Chisel, for information flow security. This thesis studies the application of secure HDLs to a prototype implementation of a commercial security architecture, ARM TrustZone. A novel architecture for information flow security called HyperFlow is presented to improve upon the shortcomings of TrustZone by providing more general security policies, constraining information release, and defending against timing-channel attacks. A second novel architecture called Timing Compartments extends HyperFlow to defend against timing-channel attacks in a multicore processor. A novel memory scheduling algorithm for preventing timing channel attacks in a shared memory controller is presented to improve performance. Overall, this thesis demonstrates that HDL-level information flow control is capable of securing usable and performant hardware designs.