Let's DOIT

This is the artifact for the paper Let’s DOIT: Using Intel’s extended HW/SW contract for secure compilation of crypto code.

Contents

This artifact contains the following directories:

• jasmin, a contribution of this work: an improved version of the Jasmin compiler
• sslh_rsb_doit, a contribution of this work, a fully protected version of libjade

• tables: in tables/main.pdf you can find results tables. The raw benchmark results are
  included under tables/data.

• intel: Scripts for extracting the Intel DOIT list of instructions along with data from the
  Wayback machiine.

• arm: Scripts for extracting tbe Arm DIT list of instructions.

• plain: libjade with no spectre protections, for comparison purposes.

• sslh: libjade with v1 protections from "Typing high-speed cryptography against spectre v1",
  for comparison purposes.

• sslh_rsb: libjade with v1 protections plus RSB from "Protecting cryptographic code against Spectre-RSB",
  for comparison purposes.

• ssbd-tools: "Tools to exercise the Linux kernel mitigation for CVE-2018-3639 (aka Variant 4)
  using the Speculative Store Bypass Disable (SSBD) feature of x86 processors", description from
  https://github.com/tyhicks/ssbd-tools

• scripts: scripts to perform several utility tasks such as preparing or running the benchmarks.

Contributions

The main contributions in this artifact are:

• Jasmin SCT type checker with support for DOIT
• High-Assurance cryptographic implementations compliant with DOIT and resistant to "all known Spectre variants"

Building Jasmin

The recommended way to build the modified Jasmin compiler is using nix; for installation
instructions of nix, see https://nixos.org/download.html
As this artifact is based on the RSB Jasmin development, it does not include
mechanized proofs of correctness.
This means that we only need to extract the compiler from Coq: to build Jasmin
using nix, run in the jasmin/ directory, the command

nix-shell --run 'cd compiler && make CIL && make'

Once the compiler is built, it is advised to put the compiler folder ($PWD/jasmin/compiler/) in your PATH
or to run, in this directory:

export JASMIN=$PWD/jasmin/compiler/jasminc
export JASMIN_CT=$PWD/jasmin/compiler/jasmin-ct

Alternatively, you can use the provided docker image to setup a configured environment with the Jasmin compiler installed:

docker build -t ches25-letsdoit:latest -f Dockerfile .
docker run -it ches25-letsdoit bash

And continuing with the reading. This process should take around 10 minutes.

Building and checking libjade

To build sslh_rsb_doit/src/libjade.a

make -C sslh_rsb_doit/src -j$(nproc) libjade.a

Note: you can omit -j$(nproc) if you wish to not use more than one job.

You can now use the library, sslh_rsb_doit/src/libjade.a, and the corresponding header file,
sslh_rsb_doit/src/libjade.h in your projects.

After libjade is compiled, you can still find all the compiled assembly files (for instance, to use
them individually) by running:

find sslh_rsb_doit/ -name "*.s"

Note: for the object files, replace *.s by *.o.

Each assembly file has a corresponding header file, include/api.h. These can be found with:

find sslh_rsb_doit/ -name "api.h"

To check security:

make -C sslh_rsb_doit/src -j$(nproc) CI=1 sct
make -C sslh_rsb_doit/src -j$(nproc) CI=1 reporter_sct

The first command runs the SCT checker on the source code and stores the logs into *.sct files.
These can be found with find sslh_rsb_doit/ -name "*.sct".

The second command reports about the status of the security checking: you should observe all
implementations tagged as "OK". Note, if you run the second command twice, on the second time
it will show nothing: the default behavior is to delete all OK files for the developer to
focus on the ERRor files. To avoid this behavior, and always show the OK files, you can add
CICL=0 to the command to prevent this cleaning from happening,
make -C sslh_rsb_doit/src -j$(nproc) CI=1 CICL=0 reporter_sct.

If you encounter a scenario where reporter_sct only reports errors, that might mean a problem
with the system's configuration; for example, jasmin-ct is not being found.

The exit code is stored in the .error files in case of a problem. By default, stderr is
redirected to the corresponding .sct file (which sits one directory above the error file).
Under normal circumstances, the .sct files contain the result of the SCT+DOIT analysis for
both possible cases: OK and ERROR. Always check the corresponding .error and .sct files
in case of an error.

To perform a complete cleanup:

If you encountered problems with your configuration (and, for example, in the meantime, fixed them),
updated the compiler, or performed significant changes in your system, it is advisable to run
distclean to ensure you start the analysis/compilation from a clean state.

make -C sslh_rsb_doit/src -j$(nproc) CI=1 distclean

Benchmarking

Preparation

Before running the benchmarks, ensure that the machine is configured for this purpose to get
stable results. This step might include disabling Turbo Boost/setting the CPU to the base
frequency/disabling Hyper-Threading/disabling efficient cores.

Run:

./scripts/bench-prepare

./scripts/bench-prepare creates a directory named bench-prepared (and a corresponding
bench-prepared.tar.bz2 if you wish to easily send this file into a machine that does not
have the Jasmin compiler configured and run the benchmarks there).

Note: if you are in a docker container but would like to run the benchmarks on the host
machine, or some other machine, you can exit the docker by typing $ exit and then copy
the bench-prepared directory with:

docker cp unruffled_curran:/home/ches25/bench-prepared bench-prepared-in-docker

Where unruffled_curran should be replaced by the container name, which can be obtained by
running docker ps -a.

Running a simple benchmark first

To run, for instance, the Kyber768 benchmark, let's say, 11 times, and each time measuring
10000 executions, and filter by keypair using grep and sorting by the number of cycles
using sort, run:

cd bench-prepared/sslh_rsb_doit/bench
make bin/crypto_kem/kyber/kyber768/amd64/avx2/bench DEFINE="-DRUNS=11 -DTIMINGS=10000"
bin/crypto_kem/kyber/kyber768/amd64/avx2/bench - | grep keypair | sort -t, -k1

You can try the same for enc or dec (with grep enc or grep dec).

Running the complete benchmark setup

cd bench-prepared/
./bench-run

After changing directories with cd bench-prepared/, or with cd bench-prepared-in-docker if
you switched machines in the meantime, you can run the benchmarks with ./bench-run: it can
take up to one hour.

To include the benchmark results into the tables/main.pdf file (where CPU is the name of your CPU),
create the tables/data/raw/USER directory:

cp -r results/* ../tables/data/raw/USER
make -C ../tables/ all

The tables/main.pdf should now contain the tables with the cycle counts.

Note: This docker image does not contain LaTeX, you will not be able to compile
tables/main.pdf inside the container without installing it.