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 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 48 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-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 |
| 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 | |
| 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 | |
| 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 |
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
- Blog: The state of tooling for verifying constant-timeness of cryptographic implementations
- “They’re not that hard to mitigate”: What Cryptographic Library Developers Think About Timing Attacks
- Blog: Testing constant-timeness using Valgrind: case of the NSS library
- Blog: Constant-time code verification with Memory Sanitizer
