Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Thu 21 Jan 2021 16:40 - 16:50 at POPL-A - Security

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 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 17:00: SecurityPOPL at POPL-A
16:00 - 16:10
Talk
Efficient and Provable Local Capability Revocation using Uninitialized Capabilities
POPL
Aina Linn GeorgesAarhus University, Armaël GuéneauAarhus University, Thomas Van StrydonckKULeuven, Amin TimanyAarhus University, Alix TrieuAarhus University, Sander HuyghebaertVrije Universiteit Brussel, Dominique DevrieseVrije Universiteit Brussel, Lars BirkedalAarhus University
Link to publication DOI Pre-print
16:10 - 16:20
Talk
Mechanized Logical Relations for Termination-Insensitive Noninterference
POPL
Simon Oddershede GregersenAarhus University, Johan BayAarhus University, Amin TimanyAarhus University, Lars BirkedalAarhus University
Link to publication DOI Pre-print
16:20 - 16:30
Talk
Giving Semantics to Program-Counter Labels via Secure Effects
POPL
Andrew HirschMax Planck Institute for Software Systems, Ethan CecchettiCornell University
Link to publication DOI
16:30 - 16:40
Talk
Automata and Fixpoints for Asynchronous Hyperproperties
POPL
Jens Oliver GutsfeldWestfälische Wilhelm-Universität Münster (WWU), Germany, Markus Müller-OlmUniversity of Münster, Christoph OhremWestfälische Wilhelms-Universität Münster (WWU), Germany
Link to publication DOI
16:40 - 16:50
Talk
Automatically Eliminating Speculative Leaks from Cryptographic Code with BladeDistinguished Paper
POPL
Marco VassenaCISPA Helmholtz Center for Information Security, Craig DisselkoenUniversity of California at San Diego, USA, Klaus v. GleissenthallVrije Universiteit Amsterdam, Netherlands, Sunjay CauligiUniversity of California at San Diego, USA, Rami Gökhan KıcıUniversity of California at San Diego, USA, Ranjit JhalaUniversity of California at San Diego, Dean TullsenUniversity of California at San Diego, USA, Deian StefanUniversity of California at San Diego, USA
Link to publication DOI Pre-print
16:50 - 17:00
Break
Break
POPL