This repo contains the benchmarks and analysis scripts used to test Blade in our paper (video here).
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
.
The instructions here should allow you to reproduce Table 1 (Section 7) in the paper.
You will need:
- This repo
lucet-blade
from https://github.com/PLSysSec/lucet-blade, on theblade
branch. Be sure to check out all submodules as well.- the WASI SDK from https://github.com/WebAssembly/wasi-sdk
- WABT from https://github.com/WebAssembly/wabt (release 1.0.15 is known to work)
- Binaryen from https://github.com/WebAssembly/binaryen (version 90 is known to work)
- HACL* from https://github.com/project-everest/hacl-star/ (commit
de6a314ab
is known to work) - Rust (e.g. from rustup)
In the Makefile
in this repo, adjust the variables at the top according to
the paths to each of these dependencies on your system.
Also adjust the Cargo.toml
in this repo if necessary, with the appropriate
path to lucet-blade
for the lucet-runtime
dependency.
Then, make build
in this repo, which should build our modified Lucet, all
of our Wasm examples, and the test framework.
In this repo, make bench
runs all of our benchmarks. This should take
around 10-20 minutes to complete.
(You may see messages about skipped tests, which is normal, or about various outliers, which is also normal.)
Then, use make report
to create the table summarizing the results. This
outputs a version of the table to stdout
, and the actual LaTeX for the
table (as presented in our paper) to ./analysis/table.tex
.
- After
make build
, you can inspect the generated x86 assembly for any of our benchmarks by runningobjdump -SDg
on the appropriate.so
file in./wasm_obj
. - You can also inspect the generated WebAssembly for any of the C-language
benchmarks by using
make wasm_wat/*
for the appropriate*
. - To compile other C code with Blade:
make build
in this repo- Compile your code to Wasm using the WASI SDK's
clang
compiler ($(WASI_SDK)/bin/clang
) and theWASI_CLANG_FLAGS
andWASI_LINK_FLAGS
from theMakefile
- Then compile these Wasm files to native code using our modified Lucet
compiler (
$(LUCET_BLADE)/target/debug/lucetc
) and theLUCETC_FLAGS
from theMakefile
. - You can choose the Blade mitigation using the
--blade-type
flag tolucetc
:- For Ref:
--blade-type=none
- For Baseline-F:
--blade-type=baseline_fence
- For Baseline-S:
--blade-type=baseline_slh
- For Blade-F:
--blade-type=lfence
- For Blade-S:
--blade-type=slh
- For Ref:
- You can also choose to enable the v1.1 mitigations with the
--blade-v1-1
flag tolucetc
(off by default).