Automatically Eliminating Speculative Leaks With Blade

We introduce BLADE, a new approach to automatically and efficiently synthesizing provably correct repairs for transient execution vulnerabilities like Spectre. BLADE is built on the insight that to stop speculative execution attacks, it suffices to cut the dataflow from expressions that speculatively introduce secrets ($\textit{sources}$) to those that leak them through the cache ($\textit{sinks}$), rather than prohibiting speculation altogether. We formalize this insight in a $\textit{static type system}$ that (1) types each expression as either $\textit{transient}$, i.e., possibly containing speculative secrets or as being $\textit{stable}$, and (2) prohibits speculative leaks by requiring that all $\textit{sink}$ expressions are stable. We introduce $\texttt{protect}$, a new abstract primitive for fine grained speculation control that can be implemented via existing architectural mechanisms, and show how our type system can automatically synthesize a $\textit{minimal}$ number of $\texttt{protect}$ calls needed to ensure the program is secure. We evaluate BLADE by using it to repair several verified, yet vulnerable WebAssembly implementations of cryptographic primitives. BLADE can fix existing programs that leak via speculation $\textit{automatically}$, without user intervention, and $\textit{efficiently}$ using two orders of magnitude fewer fences than would be added by existing compilers, and thereby ensuring security with minimal performance overhead.