Automatically eliminating speculative leaks from cryptographic code with blade
- 4 January 2021
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in Proceedings of the ACM on Programming Languages
- Vol. 5 (POPL), 1-30
- https://doi.org/10.1145/3434330
Abstract
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 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 even when using fences to implement protect.Funding Information
- NSF (CNS-1514435)
- ONR (N000141512750)
This publication has 25 references indexed in Scilit:
- ret2specPublished by Association for Computing Machinery (ACM) ,2018
- JasminPublished by Association for Computing Machinery (ACM) ,2017
- HACL*: A Verified Modern Cryptographic LibraryPublished by Association for Computing Machinery (ACM) ,2017
- Bringing the web up to speed with WebAssemblyPublished by Association for Computing Machinery (ACM) ,2017
- Efficient Cache Attacks on AES, and CountermeasuresJournal of Cryptology, 2009
- SoftBoundPublished by Association for Computing Machinery (ACM) ,2009
- Cache Attacks and Countermeasures: The Case of AESLecture Notes in Computer Science, 2006
- Enforcing robust declassificationPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2004
- Precise and efficient static array bound checking for large embedded C programsACM SIGPLAN Notices, 2004
- A lattice of informationPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002