Content area
As Moore’s Law slows, microarchitects are turning to clever and exotic microarchitectural optimizations to accelerate workloads. However, these optimizations are often data-dependent, inadvertently creating side channels that leak sensitive information. Disabling them for security is impractical. Meanwhile, security-critical software—such as cryptographic code—lacks visibility into how its execution might trigger such leaks. As these optimizations grow more complex, writing microarchitecturally safe software will only become more difficult. Defending against side-channel attacks therefore demands a holistic, cross-layer approach that bridges the hardware–software divide.
This dissertation provides a methodology, and accompanying formal analyses, to tackle the microarchitectural side channel problem. Our approach is two-pronged. First, we verify the microarchitecture, e.g., the RTL, for security. Once verified, we obtain software-facing artifacts: security-centric microarchitectural specifications. Then, we develop compiler-like frameworks that take leaky code and derived security specifications as inputs to automatically produce microarchitecture-specific code that conforms to the security specification, guaranteeing that no secrets can leak through side-channels.
We achieve this vision through three key technical contributions.
First, drawing inspiration from a variety of side-channels and defenses, we formulate an instruction set-centric definition to microarchitectural security. We articulate this as a formal property: the Safe Instruction Set Property, SISP, which guarantees that unbounded executions of a compositions of instructions do not leak secrets on the microarchitecture. Verifying if a set of instructions satisfies SISP on a microarchitecture gives us a convenient software-facing abstraction: the set of instructions that are safe to allow compute on secret data.
However, state-of-the-art verification tools do not scale to verify SISP on large hardware designs. To overcome this verification bottleneck, we develop H-Houdini, a new scalable invariant learning algorithm capable of proving properties on large hardware designs. We implement H-Houdini in tool called VeloCT: a (mostly) push-button tool to verify SISP on hardware designs. VeloCT, for the first time, is able to scale security verification to BOOM, a large open-source Out-of-Order (OoO) core, in timescales ranging from 6m to 3.3h from the smallest to the largest parameterization of BOOM. More importantly, the set of safe instructions verified by VeloCT can now be used as a software-facing abstraction to harden code.
Lastly, we develop SynthCT, a program synthesis based framework that uses the safe set specification to automatically harden security-critical code against side-channels on a specific microarchitecture. Notably, SynthCT is a robust, scalable framework that handles modern, complex ISAs like x86-64 with 1000s of instructions, and is capable of rewriting even the most complex instructions, like division (DIVL), using a set of simple safe instructions.
We believe that the combination of techniques and tools developed in this thesis can serve as a first step towards holistic, scalable, automated, principled defenses against microarchitectural side-channel attacks.