Skip to content
Snippets Groups Projects

spectre-db

A database of Intel Spectre vulnerabilities with example code.

Organisation

The project is organised as follows:

spectre-db/
├─ [variant]/
│  ├─ README.md
│  └─ [source]/
│     ├─ README.md
│     ├─ [citation].bib
│     └─ [vulnerability-alias]/
│        ├─ README.md
│        ├─ [vulnerability].c
│        ├─ [toy-semantics].thy
│        └─ [architecture-triplet]/
│           └─ [compiler]/
|              ├─ README.md
|              ├─ [vulnerability].exe
|              ├─ [vulnerability].bil
|              └─ [vulnerability].bir
├─ msvc/
|   - prebuilt x64 binaries using MSVC.
└─ README.md
  • [variant] the variant's abbreviation (according to Intel's Advisory Guidance)
  • [source] the (literature) source of the vulnerability
  • [citation] the BibTex citation
  • [vulnerability-alias] an alias this project uses to refer to the vulnerability
  • [vulnerability] a short filename for the vulnerability
  • [architecture-triplet] the architecture target as a triplet (i.e. x86_64, arm)
  • [compiler] the compiler (i.e. clang, msvc, gcc)

Compiling with MSVC

MSVC is not supported on non-windows platforms and BAP is not supported on non-linux platforms. This means that both Linux and Windows operating systems are required to generate the BIL files from C source needed for the Isabelle/HOL proofs in 'Verifying Secure Speculation in Isabelle/HOL.

In the absence of a Windows system, prebuilt binaries are distributed under ./msvc. The rest of this section can be skipped. Otherwise, the rest of this section details how to compile the examples from scratch.

Using Docker

The MSVC compiler is notoriously difficult to use, as such, we distribute a dockerfile capable of compiling the examples using the environment tested against in our paper. These are the steps to follow:

  1. Delete the prebuilt binaries in ./msvc.
  2. Ensure Docker Desktop is started with Windows containers selected.
  3. Compile the sources for Windows by running docker build -f ./Compile/Dockerfile-Msvc -t spectre-db-compile-msvc:1.0.0 ..
  • If the container fails to build you might need to play around with the versions of the Windows docker image in Dockerfile-Msvc so that it matches your host OS.
  1. Run the container with docker run -t spectre-db-compile-msvc:1.0.0.
  2. Once the container has stopped (which may take 20mins), copy the files from the container back to the host using docker cp <container-id>:C:/msvc/ ./.

Generating the BIL files

Using Docker

BAP is a lengthy and complicated install, therefore, we provide a container with BAP preinstalled which generates BIL for each of the examples.

  1. Ensure the binaries for MSVC are built and stored in the ./msvc folder at root of the repository.
  2. If using Docker Desktop for Windows ensure Linux containers are selected.
  3. Build the image by running docker build -f ./Analyse/Dockerfile-Msvc -t spectre-db-analyse-msvc:1.0.0 .
  4. Run the container with docker run -t spectre-db-analyse-msvc:1.0.0.
  5. Once the container has stopped (which may take 5mins), copy the files from the container back to the host using docker cp <container-id>:/BCB/ ./msvc/.