Constant-timeness verification tools
This page lists tools for testing and verification of constant-timeness of programs. The table is based mostly on the work in “They’re not that hard to mitigate”: What Cryptographic Library Developers Think About Timing Attacks and “These results must be false”: A usability evaluation of constant-time analysis tools with addition of more tools. Each tool has its own page with more information and resources, sometimes even a tutorial on using the tool.
There are currently 52 tools in the table.
Tools
| Name | Year | Target | Technique | Guarantees | Tutorial |
|---|---|---|---|---|---|
| Abacus | 2021 | Binary | Dynamic | sound with restrictions | |
| ABPV13 | 2013 | C | Formal | sound | |
| ABSynthe | 2020 | Binary | Dynamic | other | |
| ANABLEPS | 2019 | Binary | Dynamic | no | |
| Binsec | 2020 | Binary | Symbolic | sound with restrictions | yes |
| Blazer | 2017 | Java | Formal | sound | |
| BPT17 | 2017 | C | Symbolic | sound with restrictions | |
| Cache Templates | 2015 | Binary | Statistical | other | |
| CacheAudit | 2013 | Binary | Formal | other | |
| CacheAudit2 | 2017 | Binary | Formal | other | |
| CacheD | 2016 | Trace | Symbolic | false | |
| CacheFix | 2018 | Trace | Symbolic | sound with restrictions | |
| CacheQL | 2022 | Binary | Dynamic | sound with restrictions | |
| CacheS | 2019 | Binary | Formal | sound with restrictions | |
| CANAL | 2018 | LLVM IR | Formal | sound | |
| CaSym | 2019 | LLVM IR | Symbolic | sound | |
| CaType | 2022 | Binary | Formal | sound | |
| CHALICE | 2019 | LLVM IR | Symbolic | other | |
| COCO-CHANNEL | 2018 | Java | Symbolic | sound | |
| Constantine | 2021 | LLVM IR | Dynamic | sound with restrictions | |
| ct-fuzz | 2020 | LLVM IR | Dynamic | no | |
| CT-Prover | 2024 | LLVM IR | Formal | sound | |
| ct-verif | 2016 | LLVM IR | Formal | sound | yes |
| CT-WASM | 2019 | WASM | Formal | sound | |
| ctgrind | 2010 | Binary | Dynamic | sound with restrictions | |
| DATA | 2018 | Binary | Dynamic | sound with restrictions | |
| DifFuzz | 2019 | Java | Dynamic | no | |
| dudect | 2017 | Binary | Statistical | no | yes |
| EasyWalk-CI | 2024 | Binary | Dynamic | sound with restrictions | |
| ENCIDER | 2022 | LLVM IR | 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 | yes |
| KMO12 | 2012 | Binary | Formal | other | |
| Manifold | 2022 | Binary | Statistical | no | |
| MemSan | - | LLVM IR | Dynamic | sound with restrictions | yes |
| Microwalk | 2018 | Binary | Dynamic | sound with restrictions | |
| Pendulum | 2024 | Java | Dynamic | no | |
| Pin-based CEC | 2019 | Binary | Dynamic | sound with restrictions | |
| pitchfork-angr | 2019 | Binary | Symbolic | no | |
| SC-Eliminator | 2018 | LLVM IR | Formal | sound | |
| SideTrail | 2018 | LLVM IR | Formal | other | |
| SKKJH18 | 2018 | Binary | Statistical | no | |
| STACCO | 2017 | Binary | Dynamic | no | |
| STAnalyzer | 2017 | C | Formal | sound | |
| Themis | 2017 | Java | Formal | sound | |
| Timecop | - | Binary | Dynamic | sound with restrictions | yes |
| tis-ct | - | C | Symbolic | sound with restrictions | |
| tlsfuzzer | 2023 | Network | Statistical | other | |
| TriggerFlow | 2018 | Binary | Dynamic | no | |
| VirtualCert | 2014 | x86 | Formal | sound |
Note that the claims w.r.t. guarantees in this table are best effort and may be wrong. Many tools do not claim any guarantees about their analysis.
Examples
The following list constains short snippets of C code that exhibit constant-time (or not) behavior and can be useful for testing constant-timeness verification tools, or learning how to use them.
- 01.c (non-CT)
- 02.c (CT)
- 03.c (non-CT)
- 04.c (CT)
- 05.c (non-CT)
- 06.c (CT)
- 07.c (non-CT)
- 08.c (depends)
- 09.c (CT)
- 10.c (non-CT)
Resources
The resources below can be helpful if you are seeking more information on these tools or constant-time code in general.
- Blog: The state of tooling for verifying constant-timeness of cryptographic implementations
Constitutes a precursor to this site, some reasoning for the classification used on this site is given there. - “They’re not that hard to mitigate”: What Cryptographic Library Developers Think About Timing Attacks
Presents a survey done among cryptographic library developers into their view on timing attacks, their mitigation and constant-timeness analysis tools. - “These results must be false”: A usability evaluation of constant-time analysis tools
Presents a user study evaluating the usability of some constant-timeness analysis tools: Binsec, ct-verif, dudect, valgrind, MemSan, haybale-pitchfork. - A Systematic Evaluation of Automated Tools for Side-Channel Vulnerabilities Detection in Cryptographic Libraries
Presents a thorough and systematic classification of 34 constant-timeness analysis tools. - Blog: Testing constant-timeness using Valgrind: case of the NSS library
Case study on using Valgrind for constant-timeness analysis of the NSS library. - Blog: Constant-time code verification with Memory Sanitizer
Case study on using MemSan for constant-timeness analysis.
Miscellaneous
The articles below mostly discuss the role of compilers in introducing (and potentially mitigating) timing leaks.
- What you get is what you C: Controlling side effects in mainstream C compilers
- Breaking Bad: How Compilers Break Constant-Time Implementations
- Clang vs. Clang: You’re making Clang angry. You wouldn’t like Clang when it’s angry.
- Architectural Mimicry: Innovative Instructions to Efficiently Address Control-Flow Leakage in Data-Oblivious Programs
