We introduce Blade, a new approach to automatically and efficiently eliminate speculative leaks from cryptographic code. Blade is built on the insight that to stop leaks via speculative execution, it suffices to
cut
the dataflow from expressions that speculatively introduce secrets (
sources
) to those that leak them through the cache (
sinks
), rather than prohibit speculation altogether. We formalize this insight in a
static type system
that (1) types each expression as either
transient
, i.e., possibly containing speculative secrets or as being
stable
, and (2) prohibits speculative leaks by requiring that all
sink
expressions are stable. Blade relies on a new abstract primitive,
protect
, to halt speculation at fine granularity. We formalize and implement
protect
using existing architectural mechanisms, and show how Blade’s type system can automatically synthesize a
minimal
number of
protect
s to provably eliminate speculative leaks. We implement Blade in the Cranelift WebAssembly compiler and evaluate our approach by repairing several verified, yet vulnerable WebAssembly implementations of cryptographic primitives. We find that Blade can fix existing programs that leak via speculation
automatically
, without user intervention, and
efficiently
even when using fences to implement
protect
.