tfaoliveira/rsbsecure-asplos25 repository overview

This repository contains a docker image corresponding to the artifact of the paper: Protecting cryptographic code against Spectre-RSB:

• ASPLOS 25: https://www.asplos-conference.org/asplos2025/⁠
• https://eprint.iacr.org/2024/1070⁠
• https://artifacts.formosa-crypto.org/data/rsbsecure.tar.bz2⁠

First, get the image:

$ docker pull tfaoliveira/rsbsecure-asplos25

And create a simpler tag for the image:

$ docker tag tfaoliveira/rsbsecure-asplos25:latest rsbsecure-asplos25:latest

Now, you can copy a Makefile from the image into your host system. This Makefile defines some rules to simplify the user's life:

$ docker create --name asplos25-get-makefile rsbsecure-asplos25
$ docker cp asplos25-get-makefile:/home/asplos25/Makefile .
$ docker rm asplos25-get-makefile

To build the formalization, use the following command. It should take around 20s on a reasonably recent machine. It will create a temporary container to run the job.

$ make step1_build_formalization
(...)
Building the formalization: all OK.

Next, you can check that Libjade is speculative constant-time (including the protections against Spectre-RSB) with the following command. It takes a couple of seconds. You should be able to see "OK" messages next to the implementation full path.

$ make step2_typecheck_spectre_rsb
(...)
Typechecking Spectre: all OK.

To build libjade, you can run the following command. It will compile libjade inside a container and copy it to the host: you will see two files, libjade.a and libjade.h. It shouldn't take much longer than 30 seconds.

$ make step3_compile_libjade
(...)
Compiling libjade.a: all OK.

$ ls libjade.* 
libjade.a  libjade.h

Next, it's about benchmarks. For Spectre v4 protections, the artifact relies on ssbd-tools from https://github.com/tyhicks/ssbd-tools⁠ Concretely, the benchmarks are run using ssbd-exec to test different settings for Speculative Store Bypass Disable. Take a look into the section Why SSBD may not be available⁠. There's a chance you might need to perform a firmware update.

For simplicity, we first explain how to run the benchmarks inside a container and then outside of it. Running the benchmarks takes around one hour.

The following command runs the benchmark inside a container. When the benchmarks are completed, a PDF file will be created and copied to the host machine. This file contains the CPU cycle counts for the CPU used in the paper and the 'default' CPU, corresponding to your CPU.

$ make step4A_run_benchmark_inside_docker
(...)
Benchmarking: all OK.
$ ls *.pdf
asplos25-tables.pdf
$ docker ps -a 
(...) asplos25-benchmark-libjade

The container is not deleted by the step4A rule. You can use docker exec to inspect its contents before deleting it with $ make step5A_remove_benchmark_container. For instance, several benchmarking results don't go into the tables, and you can easily find them inside the container with find . -name "*.csv".

To run the benchmarks outside of the docker container, you can start by running:

$ make step4B_prepare_benchmark_to_run_on_the_host
$ ls *.tar.bz2
bench-prepared.tar.bz2

This command will create a file bench-prepared.tar.bz2 that you can use on some machine with (or $ make step5B_run_benchmark_on_the_host):

$ tar xjf bench-prepared.tar.bz2
$ cd bench-prepared/
$ ./bench-run

To copy back the results in to a container to produce the PDF file run:

$ make step6B_copy_results_into_container

If containers are lying around, run make clean_all_containers.