Binsec/Haunted is a binary-analysis tool for speculative constant-time, that can find Spectre-PHT (a.k.a. Spectre-v1) and Spectre-STL (a.k.a. Spectre-v4) vulnerabilities in binary code.

It is an extension of the binary analysis plateform Binsec, and in particular, it builds on its module for relational symbolic execution, Binsec/Rel.

If you are interested, you can read the paper, published at NDSS 2021.

Benchmarks to test Binsec/Haunted: https://github.com/binsec/haunted_bench

The docker contains necessary files for running Binsec/Haunted and the benchmarks to test it.

1. Download the image.

2. Import the image:

 docker load < binsec-haunted.tar 

3. Run the container:

docker run -it binsec-haunted /bin/bash 

4. Run ./update.sh to get the latest version of Binsec/Haunted.

5. You are ready to go! Look at Readme.md or read the documentation of Binsec/haunted_bench for examples on how to use Binsec/Haunted.

Requirements: boolector (recommended boolector-3.2.0), z3, yices or cvc4.

# Install Ocaml and prerequisite packages for BINSEC via OPAM sudo apt update sudo apt install ocaml ocaml-native-compilers camlp4-extra opam protobuf-compiler libgmp-dev libzmq3-dev llvm-6.0-dev cmake pkg-config opam init opam switch 4.05.0 opam install menhir.20211012 ocamlgraph piqi zarith zmq.5.0.0 llvm.6.0.0 oUnit hashset containers # Additional packages (optional) # opam install merlin ocp-indent caml-mode tuareg ocamlfind # Checkout source code git clone https://github.com/binsec/haunted.git binsec-haunted # Compile source code cd binsec-haunted autoconf ./configure cd src make depend make binsec

Print the help:

$ binsec --help

Source code of Binsec/Haunted is located under src/relse/.