Skip to the content.

Constant-timeness verification tools

This page lists tools for testing and verification of constant-timeness of programs.

Oprah giving everyone a tool

Tools

Name Year Target Technique Guarantees
Abacus 2021 Binary Dynamic sound with restrictions
ABPV13 2013 C Formal sound
ANABLEPS 2019 Binary Dynamic no
Binsec/Rel 2020 Binary Symbolic sound with restrictions
Blazer 2017 Java Formal sound
BPT17 2017 C Symbolic sound with restrictions
CacheAudit 2013 Binary Formal other
CacheQL 2022 Binary Dynamic sound with restrictions
CacheD 2016 Trace Symbolic no
CacheS 2019 Binary Formal sound with restrictions
CacheFix 2018      
CANAL 2018 LLVM IR Formal  
CaSym 2019 LLVM IR Symbolic sound
CaType 2022 Binary Formal sound
CHALICE 2019      
COCO-CHANNEL 2018 Java Symbolic sound
Constantine 2021      
ctgrind 2010 Binary Dynamic sound with restrictions
ct-fuzz 2020 LLVM IR Dynamic no
ct-verif 2016 LLVM IR Formal sound
CT-WASM 2019 WASM Formal sound
DATA 2018 Binary Dynamic sound with restrictions
dudect 2017 Binary Statistical no
ENCIDER 2022 LLVM Symbolic sound with restrictions
ENCoVer 2012 Java Formal sound
FaCT 2019 DSL Formal sound
FlowTracker 2016 LLVM IR Formal sound
haybale-pitchfork 2019 LLVM IR Symbolic sound with restrictions
KMO12 2012 Binary Formal other
Manifold 2022      
MemSan - LLVM IR Dynamic sound with restrictions
MicroWalk 2018 Binary Dynamic sound with restrictions
pitchfork-angr 2019      
SC-Eliminator 2018 LLVM IR Formal sound
SideTrail 2018 LLVM IR Formal other
Themis 2017 Java Formal sound
timecop - Binary Dynamic sound with restrictions
tis-ct - C Symbolic sound with restrictions
TriggerFlow 2018      
VirtualCert 2014 x86 Formal sound

This table is based mostly on the work in “They’re not that hard to mitigate”: What Cryptographic Library Developers Think About Timing Attacks with manual addition of more tools.

Abacus

ABPV13

ANABLEPS

Binsec/Rel

Blazer

BPT17

CacheAudit

CacheQL

CacheD

CacheS

CacheFix

CANAL

CaSym

CHALICE

CaType

COCO-CHANNEL

Constantine

ctgrind

ct-fuzz

ct-verif

CT-WASM

DATA

dudect

ENCIDER

ENCoVer

FaCT

FlowTracker

haybale-pitchfork

KMO12

Manifold

MemSan

MicroWalk

pitchfork-angr

SC-Eliminator

SideTrail

Themis

timecop

tis-ct

TriggerFlow

VirtualCert

Resources