Automatically Eliminating Speculative Leaks from Cryptographic Code with BladeDistinguished Paper
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 new abstract primitive, protect, to halt speculation at fine granularity. We formalize and implement protect using existing architectural mechanisms, and show how Blade type system can automatically synthesize a minimal number of protects 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, imposing less than 20% overhead even when using fences to implement protect.
Thu 21 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:00 - 17:00 | |||
16:00 10mTalk | Efficient and Provable Local Capability Revocation using Uninitialized Capabilities POPL Aina Linn Georges Aarhus University, Armaël Guéneau Aarhus University, Thomas Van Strydonck KULeuven, Amin Timany Aarhus University, Alix Trieu Aarhus University, Sander Huyghebaert Vrije Universiteit Brussel, Dominique Devriese Vrije Universiteit Brussel, Lars Birkedal Aarhus University Link to publication DOI Pre-print | ||
16:10 10mTalk | Mechanized Logical Relations for Termination-Insensitive Noninterference POPL Simon Oddershede Gregersen Aarhus University, Johan Bay Aarhus University, Amin Timany Aarhus University, Lars Birkedal Aarhus University Link to publication DOI Pre-print | ||
16:20 10mTalk | Giving Semantics to Program-Counter Labels via Secure Effects POPL Link to publication DOI | ||
16:30 10mTalk | Automata and Fixpoints for Asynchronous Hyperproperties POPL Jens Oliver Gutsfeld Westfälische Wilhelm-Universität Münster (WWU), Germany, Markus Müller-Olm University of Münster, Christoph Ohrem Westfälische Wilhelms-Universität Münster (WWU), Germany Link to publication DOI | ||
16:40 10mTalk | Automatically Eliminating Speculative Leaks from Cryptographic Code with BladeDistinguished Paper POPL Marco Vassena CISPA Helmholtz Center for Information Security, Craig Disselkoen University of California at San Diego, USA, Klaus v. Gleissenthall Vrije Universiteit Amsterdam, Netherlands, Sunjay Cauligi University of California at San Diego, USA, Rami Gökhan Kıcı University of California at San Diego, USA, Ranjit Jhala University of California at San Diego, Dean Tullsen University of California at San Diego, USA, Deian Stefan University of California at San Diego, USA Link to publication DOI Pre-print | ||
16:50 10mBreak | Break POPL | ||