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:
- Delete the prebuilt binaries in
./msvc
. - Ensure Docker Desktop is started with Windows containers selected.
- 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.
- Run the container with
docker run -t spectre-db-compile-msvc:1.0.0
. - 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.
- Ensure the binaries for MSVC are built and stored in the
./msvc
folder at root of the repository. - If using Docker Desktop for Windows ensure Linux containers are selected.
- Build the image by running
docker build -f ./Analyse/Dockerfile-Msvc -t spectre-db-analyse-msvc:1.0.0 .
- Run the container with
docker run -t spectre-db-analyse-msvc:1.0.0
. - 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/
.