Data

Tools

Indexes

Applications

Experiments

Open Source Science

https://github.com/binsec/haunted

Binsec/Haunted is an extension of Binsec to verify speculative constant-time and detect Spectre attacks.

https://github.com/binsec/haunted

Science Score: 10.0%

This score indicates how likely this project is to be science-related based on various indicators:

  • ○
    CITATION.cff file
  • ○
    codemeta.json file
  • ○
    .zenodo.json file
  • ○
    DOI references
  • ✓
    Academic publication links
    Links to: zenodo.org
  • ○
    Academic email domains
  • ○
    Institutional organization owner
  • ○
    JOSS paper metadata
  • ○
    Scientific vocabulary similarity
    Low similarity (10.0%) to scientific vocabulary

Keywords

binary-analysis spectre-vulnerability symbolic-execution
Last synced: 5 months ago · JSON representation

Repository

Binsec/Haunted is an extension of Binsec to verify speculative constant-time and detect Spectre attacks.

Basic Info
  • Host: GitHub
  • Owner: binsec
  • License: lgpl-2.1
  • Language: OCaml
  • Default Branch: master
  • Homepage:
  • Size: 860 KB
Statistics
  • Stars: 15
  • Watchers: 5
  • Forks: 1
  • Open Issues: 1
  • Releases: 0
Topics
binary-analysis spectre-vulnerability symbolic-execution
Created about 5 years ago · Last pushed over 2 years ago
Metadata Files
Readme Changelog License

Readme.md

Binsec/Haunted: a binary-level analyzer to detect vulnerabilities to Spectre attacks.

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

Installation

Docker

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.

From sources

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

``` bash

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: bash $ binsec --help

Source code

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

Owner

  • Name: BINSEC development team
  • Login: binsec
  • Kind: organization

GitHub Events

Total
  • Watch event: 1
Last Year
  • Watch event: 1