Skip to the content.

Constant-timeness verification tools

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

Tools

Name Year Target Technique Guarantees
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
CacheD 2016 Trace Symbolic no
CacheS 2019 Binary Formal sound with restrictions
CacheFix 2018      
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
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.

ABPV13

ANABLEPS

Binsec/Rel

Blazer

BPT17

CacheAudit

CacheD

CacheS

CacheFix

COCO-CHANNEL

Constantine

ctgrind

ct-fuzz

ct-verif

CT-WASM

DATA

dudect

ENCIDER

ENCoVer

FaCT

FlowTracker

haybale-pitchfork

KMO12

MemSan

MicroWalk

pitchfork-angr

SC-Eliminator

SideTrail

Themis

timecop

tis-ct

TriggerFlow

VirtualCert

Resources