(POPL 2021) Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade
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 \emph{cut} the dataflow from expressions that speculatively introduce secrets (\emph{sources}) to those that leak them through the cache (\emph{sinks}), rather than prohibit speculation altogether. We formalize this insight in a \emph{static type sytem} that (1) types each expression as either \emph{transient}, i.e., possibly containing speculative secrets or as being \emph{stable}, and (2) prohibits speculative leaks by requiring that all \emph{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 \emph{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 \emph{automatically}, without user intervention, and \emph{efficiently}, imposing less than 20% overhead even when using fences to implement protect.
Wed 15 JunDisplayed time zone: Pacific Time (US & Canada) change
13:30 - 14:50 | |||
13:30 20mTalk | (OOPSLA 2021) Reconciling Optimization with Secure Compilation SIGPLAN Track Son Tuan Vu Sorbonne Université, CNRS, Laboratoire d'Informatique de Paris 6, LIP6, Albert Cohen Google, Arnaud de Grandmaison , Christophe Guillon STMicroelectronics, Karine Heydemann Sorbonne University; CNRS; LIP6 Link to publication DOI Authorizer link Pre-print | ||
13:50 20mTalk | (PLDI 2020) Constant-Time Foundations for the New Spectre Era SIGPLAN Track Sunjay Cauligi University of California at San Diego, USA, Craig Disselkoen University of California at San Diego, USA, Klaus v. Gleissenthall Vrije Universiteit Amsterdam, Netherlands, Dean Tullsen University of California at San Diego, USA, Deian Stefan University of California at San Diego, Tamara Rezk INRIA, Gilles Barthe MPI-SP, Germany / IMDEA Software Institute, Spain | ||
14:10 20mTalk | (PLDI 2020) SCAF: A Speculation-Aware Collaborative Dependence Analysis Framework SIGPLAN Track Sotiris Apostolakis Google, Ziyang Xu Princeton University, Zujun Tan Princeton University, USA, Greg Chan Princeton University, USA, Simone Campanoni Northwestern University, USA, David I. August Princeton University | ||
14:30 20mTalk | (POPL 2021) Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade SIGPLAN Track Marco Vassena Utrecht University, 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; Amazon Web Services, Dean Tullsen University of California at San Diego, USA, Deian Stefan University of California at San Diego | ||