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