Spectector is a tool for reasoning about information flows produced by speculatively executed instructions. It takes as input an x64 assembly program (in the Intel or AT&T syntax), and it automatically detects leaks introduced by speculatively executed instructions (or proves their absence).
In a nutshell, Spectector symbolically executes the program under analysis with respect to a semantics that accounts for the speculative execution's effects. During the symbolic execution, Spectector derives SMT formulae characterizing leaks caused by speculatively executed instructions. It then relies on the Z3 SMT solver to determine the presence of possible leaks. More precisely, Spectector automatically proves whether a program satisfies speculative non-interference, a security property formalized in the Spectector's paper.
Using Spectector, we detected subtle bugs in the way countermeasures are placed by several major compilers, which may result in insecure programs or unnecessary countermeasures. See the Spectector's paper for more information.
Spectector is written using the Prolog dialect supported by the Ciao system, and it needs the Ciao environment to compile. Additionally, Spectector uses the Z3 SMT solver to check the satisfiability of formulae.
We have tested Spectector with Ciao version 1.18 and Z3 version 4.8.4 on Debian Linux (kernel 4.9.110), Arch Linux (kernel 4.19.4), Mac OSX (version 10.14), and Windows 10 Pro (using the Windows Linux Subsystem with kernel 4.4.0).
Build and installation
Once the Ciao system is installed, you can automatically fetch, build, and install Spectector using:
ciao get github.com/spectector/spectector
The following dependencies (including third-party code) will be installed automatically:
- Concolic for
SMT-enhanced symbolic reasoning and search
ciao get concolic). This will automatically install Z3.
- muASM translator
for muASM translation from x64 assembly (
ciao get github.com/spectector/muasm_translator)
All code will be downloaded and built under the first directory
specified in the
CIAOPATH environment variable or
Spectector can be executed over x64 assembly programs. Additionally, Spectector can analyze programs written in muASM, a simple assembly language described in the Spectector's paper.
Spectector treats each file with extension
.s as an x64 program
written using the AT&T syntax, each file with extension
.asm as an
x64 program written using the Intel syntax, and each file with
.muasm as a muASM program.
Once correctly installed, Spectector can be run from the command line as follows:
spectector assembly.file -c initConf --low policy
In the above command,
initConf is a file containing the initial configuration
policy is a file specifying the security policy:
An initial configuration specifies the initial values for some of the registers and memory locations. Spectector will treat all uninitialized registers and memory locations as containing symbolic values. We specify the initial configuration as
Memorymaps memory locations to values and
Assignmentsmaps registers to values. For instance,
c([500=0,501=0],[rax=20, pc=START])denotes that (1) the initial values of the memory locations
0, (2) the initial value of the register
20, and (3) the initial value of the program counter register
pcis the line number of the instruction labelled with
A policy specifies which registers and memory locations are known or controlled by an attacker (i.e., they contain public information). The file
policycontains a list of register identifiers and memory locations separated by a comma. For instance, the policy
[pc, rax, 500]states that the registers
raxand the memory location
500contain public information.
See the output of
spectector -h for more detailed instructions.
Supported x64 instructions and other limitations
See Sections VI.C and VIII of the Spectector's paper for a description of the supported instructions and limitations.
- This is the research paper describing Spectector.
- This file describes how to compile Spectector from source code.
- This file describes a few ways of obtaining assembly programs.
- This repository contains the benchmarks from the Spectector's paper, and it describes how to reproduce all the results therein.
- This file describes how to generate Spectector's artifact evaluation distribution.
Spectector is not production ready. It's a research prototype that demonstrates the viability of detecting speculative information flows in small assembly programs. It cannot be used (yet!) to detect speculative leaks in large, real-world programs.