Constant-timeness verification tools
This page lists tools for testing and verification of constant-timeness of programs.
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
- Introduced in “Abacus: A Tool for Precise Side-Channel Analysis” by Q. Bao, Z. Wang, J. R. Larus, and D. Wu; https://doi.org/10.1109/ICSE-Companion52605.2021.00110
- Tool available: https://github.com/s3team/Abacus
ABPV13
- Introduced in “Formal verification of side-channel countermeasures using self-composition” by J. B. Almeida, M. Barbosa, J. S. Pinto, and B. Vieira; https://doi.org/10.1016/j.scico.2011.10.008
- Tool not available
ANABLEPS
- Introduced in “Time and Order: Towards Automatically Identifying Side-Channel Vulnerabilities in Enclave Binaries” by W. Wang, Y. Zhang, and Z. Lin; https://www.usenix.org/conference/raid2019/presentation/wang-wubing
- Tool available: https://github.com/OSUSecLab/ANABLEPS
Binsec/Rel
- Introduced in “Binsec/rel: Efficient relational symbolic execution for constant-time at binary-level” by L. Daniel, S. Bardin, and T. Rezk; https://doi.org/10.1109/SP40000.2020.00074
- Tool available: https://github.com/binsec/Rel
- Tests available: https://github.com/binsec/rel_bench
- Binsec/Rel is a static analysis tool that works on the binary level, thereby overcoming issues of compilers inserting non-constant-time code or turning constant-time code into non-constant-time one.
Blazer
- Introduced in “Decomposition instead of self-composition for proving the absence of timing channels” by T. Antonopoulos, P. Gazzillo, M. Hicks, E. Koskinen, T. Terauchi, and S. Wei; https://doi.org/10.1145/3062341.3062378
- Tool not available
BPT17
- Introduced in “Verifying constant-time implementations by abstract interpretation” by S. Blazy, D. Pichardie, and A. Trieu; https://doi.org/10.1007/978-3-319-66402-6_16
- Tool available: http://irisa.fr/celtique/ext/esorics17/
CacheAudit
- Introduced in “CacheAudit: A tool for the static analysis of cache side channels” by G. Doychev, D. Feld, B. Köpf, L. Mauborgne, and J. Reineke; https://www.usenix.org/conference/usenixsecurity13/technical-sessions/paper/doychev
- Tool available: https://github.com/cacheaudit/cacheaudit
- Website: https://software.imdea.org/projects/cacheaudit/
CacheQL
- Introduced in “CacheQL: Quantifying and Localizing Cache Side-Channel Vulnerabilities in Production Software” by Y. Yuan, Z. Liu, and S. Wang; https://arxiv.org/abs/2209.14952
- Tool (will be) availablle: https://github.com/Yuanyuan-Yuan/CacheQL
CacheD
- Introduced in “Cached: Identifying cache-based timing channels in production software” by S. Wang, P. Wang, X. Liu, D. Zhang, and D. Wu; https://www.usenix.org/conference/usenixsecurity17/technical-sessions/presentation/wang-shuai
- Tool not available
CacheS
- Introduced in “Identifying cache-based side channels through secret-augmented abstract interpretation” by S. Wang, Y. Bao, X. Liu, P. Wang, D. Zhang, and D. Wu; https://www.usenix.org/conference/usenixsecurity19/presentation/wang-shuai
- Tool not available
CacheFix
- Introduced in “Symbolic verification of cache side-channel freedom” by S. Chattopadhyay and A. Roychoudhury; https://doi.org/10.1109/TCAD.2018.2858402
- Tool available: https://bitbucket.org/sudiptac/cachefix/src/master/
CANAL
- Introduced in “CANAL: a cache timing analysis framework via LLVM transformation” by C. Sung, B. Paulsen, and C. Wang; https://dl.acm.org/doi/10.1145/3238147.3240485
- Tool available: https://github.com/canalcache/canal
CaSym
- Introduced in “CaSym: Cache Aware Symbolic Execution for Side Channel Detection and Mitigation” by R. Brotzman, S. Liu, D. Zhang, G. Tan, M. Kandemir; https://doi.org/10.1109/SP.2019.00022
- Tool not available
CHALICE
- Introduced in “Quantifying the Information Leakage in Cache Attacks via Symbolic Execution” by S. Chattopadhyay, M. Beck, A. Rezine, and A. Zeller; https://dl.acm.org/doi/10.1145/3288758
- Tool available: https://bitbucket.org/sudiptac/chalice
CaType
- Introduced in “Cache Refinement Type for Side-Channel Detection of Cryptographic Software” by K. Jiang, Y. Bao, S. Wang, Z. Liu, and T. Zhang; https://arxiv.org/abs/2209.04610v2
- Tool not available
COCO-CHANNEL
- Introduced in “Symbolic path cost analysis for side-channel detection” by T. Brennan, S. Saha, T. Bultan, and C. S. Pasareanu; https://doi.org/10.1145/3213846.3213867
- Tool not available
Constantine
- Introduced in “Constantine: Automatic side-channel resistance using efficient control and data flow linearization” by P. Borrello, D. C. D’Elia, L. Querzoni, and C. Giuffrida; https://arxiv.org/abs/2104.10749
- Tool available: https://github.com/pietroborrello/constantine
ctgrind
- Introduced in https://github.com/agl/ctgrind and https://www.imperialviolet.org/2010/04/01/ctgrind.html.
- ctgrind is a patch available for the Valgrind (memcheck) tool, which adds functionality to mark areas of memory as uninitialized. This is to be used on secrets. At runtime, the memcheck tool then checks that the secret(uninitialized) memory is not used in branches or for memory access. As Valgrind’s memcheck supports the
VALGRIND_MAKE_MEM_UNDEFINED
andVALGRIND_MAKE_MEM_DEFINED
client requests, it is now possible to implement a ctgrind-like approach without patches to Valgrind. - Tool available: Use Valgrind directly.
ct-fuzz
- Introduced in “ct-fuzz: Fuzzing for timing leaks” by S. He, M. Emmi, and G. F. Ciocarlie; https://doi.org/10.1109/ICST46399.2020.00063
- ct-fuzz takes inspiration from ct-verif in its method but diverges significantly. It first constructs a product program using self-composition of the target with itself, where it asserts that at each point that the memory address accessed by the two programs, whether through control from or indexing, is the same. It then uses a fuzzer against this product program, which splits its fuzzing input equally into the secret inputs for the two instances or the original program in the product program. If the fuzzer detects a failed assert, leakage is detected, as it found two runs through the target, which differ only in secret inputs yet access different offsets in memory.
- Tool available: https://github.com/michael-emmi/ct-fuzz
ct-verif
- Introduced in “Verifying Constant-Time Implementations” by J. B. Almeida, M. Barbosa, G. Barthe, F. Dupressoir and M. Emmi; https://www.usenix.org/system/files/conference/usenixsecurity16/sec16_paper_almeida.pdf
- The ct-verif tool is a static analysis tool verifying constant-time properties of code, working on the level of LLVM IR, with source code annotations. It uses the SMACK modular software verification toolchain, Bam-Bam-Boogieman for Boogie source transformation, Boogie intermediate verification language as well as the Corral and Z3 solvers.
- The tool is actively deployed in the CI of Amazon’s s2n library at link. However, even there, it is only used to verify two functions that together have less than 100 lines of code.
- Tool available: https://github.com/imdea-software/verifying-constant-time
CT-WASM
- Introduced in “CT-WASM: type-driven secure cryptography for the web ecosystem” by C. Watt, J. Renner, N. Popescu, S. Cauligi, and D. Stefan; https://doi.org/10.1145/3290390
- Tool available: https://github.com/PLSysSec/ct-wasm
DATA
- Introduced in “DATA - differential address trace analysis: Finding address-based side-channels in binaries” by S. Weiser, A. Zankl, R. Spreitzer, K. Miller, S. Mangard, and G. Sigl; https://www.usenix.org/conference/usenixsecurity18/presentation/weise
- Used in “Big numbers - big troubles: Systematically analyzing nonce leakage in (EC)DSA implementations” by S. Weiser, D. Schrammel, L. Bodner, and R. Spreitzer; https://www.usenix.org/conference/usenixsecurity20/presentation/weiser
- DATA (Differential Address Trace Analysis) is a tool quite similar to the Microwalk framework in that it is a dynamic tool that records memory-accesses of the target into address traces as it processes random secret inputs. The traces are then aligned and analyzed using generic and specific leakage tests. The tool reports the location of leakage and even offers a graphical user interface for analysis.
- Tool available: https://github.com/Fraunhofer-AISEC/DATA
dudect
- Introduced in “Dude, is my code constant time?” by O. Reparaz, J. Balasch, and I. Verbauwhede; https://doi.org/10.23919/DATE.2017.7927267
- dudect is a dynamic tool that uses leakage assessment techniques from physical (power and EM) side-channel analysis, namely test-vector leakage assessment (TVLA). It first runs the target using two classes of secret input data with varying public input data and measures the duration of execution for each run. It then applies a test to the two distributions of the duration of execution for the two classes (either Welch’s t-test for equality of means or Kolmogorov-Smirnov test for equality of distributions), and if the distributions differ, leakage is reported. This is analogous to how leakage assessment is used in power side-channel attacks, in that instead of comparing distributions of power consumption at points during the execution of the target, the runtime distributions are compared.
- Tool available: https://github.com/oreparaz/dudect
ENCIDER
- Introduced in “ENCIDER: Detecting Timing and Cache Side Channels in SGX Enclaves and Cryptographic APIs” by Tuba Yavuz, Farhaan Fowze, Grant Hernandez, Ken Yihang Bai, Kevin Butler, and Dave Jing Tian; https://ieeexplore.ieee.org/abstract/document/9737388
- Tool not yet available: https://github.com/sysrel/ENCIDER
ENCoVer
- Introduced in “ENCoVer: Symbolic exploration for information flow security” by M. Balliu, M. Dam, and G. L. Guernic; https://doi.org/10.1109/CSF.2012.24
- Tool available: https://people.kth.se/~musard/files/encover.html
FaCT
- Introduced in “FaCT: a DSL for timing-sensitive computation” by S. Cauligi, G. Soeller, B. Johannesmeyer, F. Brown, R. S. Wahby, J. Renner, B. Grégoire, G. Barthe, R. Jhala, and D. Stefan; https://doi.org/10.1145/3314221.3314605
- The FaCT tool is less of a tool for analysis of implementations for timing leakage and more of a domain-specific language for writing constant-time implementations that automatically removes leakage during compilation. The language is C-like, compiles into LLVM IR, and offers the
secret
keyword, which is used to mark certain variables as secret, which then triggers the compiler to generate constant-time code with regards to their values. - Tool available: https://github.com/plsyssec/fact
FlowTracker
- Introduced in “Sparse representation of implicit flows with applications to side-channel detection” by B. Rodrigues, F. M. Q. Pereira, and D. F. Aranha; https://doi.org/10.1145/2892208.2892230
- The FlowTracker tool is a static tool that works by analyzing the Program Dependence Graph (PDG) of the target in LLVM IR form.
- Tool not available: http://cuda.dcc.ufmg.br/flowtracker/
haybale-pitchfork
- Introduced in https://github.com/PLSysSec/haybale-pitchfork
- Tool available: https://github.com/PLSysSec/haybale-pitchfork
KMO12
- Introduced in “Automatic quantification of cache side-channels” by B. Köpf, L. Mauborgne, and M. Ochoa; https://doi.org/10.1007/978-3-642-31424-7_40
- Tool not available, superseded by CacheAudit
Manifold
- Introduced in “Automated side channel analysis of media software with manifold learning” by Y. Yuan, Q. Pang, and S. Wang; https://www.usenix.org/conference/usenixsecurity22/presentation/yuan-yuanyuan
- Tool available: https://zenodo.org/record/5816702#.YdQMHxNByjA
MemSan
- Introduced in https://clang.llvm.org/docs/MemorySanitizer.html
- Tool available: Use MemorySanitizer.
MicroWalk
- Introduced in “Microwalk: A framework for finding side channels in binaries” by J. Wichelmann, A. Moghimi, T. Eisenbarth, and B. Sunar; https://doi.org/10.1145/3274694.3274741
- The MicroWalk framework is a dynamic tool that uses Dynamic Binary Instrumentation (DBI) and Mutual Information Analysis (MIA). As a dynamic tool, it runs the target with random inputs and uses dynamic binary instrumentation to log events such as memory allocations, branches, calls, returns, memory reads/writes as well as stack operations into an execution trace. It then processes these traces by applying the chosen leakage model, i.e., in the branching model, it only keeps the control flow events in the execution traces. After collection of traces, it offers several analysis options, either directly comparing the traces or using mutual information analysis either on the whole trace or a specific offset in the execution traces (a specific instruction).
- Tool available: https://github.com/UzL-ITS/Microwalk
pitchfork-angr
- Introduced in https://github.com/PLSysSec/pitchfork-angr
- Tool available: https://github.com/PLSysSec/pitchfork-angr
SC-Eliminator
- Introduced in “Eliminating timing side-channel leaks using program repair” by M. Wu, S. Guo, P. Schaumont, and C. Wang; https://doi.org/10.1145/3213846.3213851
- Tool available: https://zenodo.org/record/1299357
SideTrail
- Introduced in “Sidetrail: Verifying time-balancing of cryptosystems” by K. Athanasiou, B. Cook, M. Emmi, C. MacCárthaigh, D. Schwartz-Narbonne, and S. Tasiran; https://doi.org/10.1007/978-3-030-03592-1_12
- SideTrail (at one point called SideWinder) is a tool for verifying time-balanced implementations. The notion of time-balance is a weakening of the constant-time notion that allows for the presence of leakage that is provably under some bound $\delta$ (execution time is negligibly influenced by secrets). For $\delta = 0$ this notion fits well with the notion of constant-time. The tool uses a cross-product technique similar to that of ct-verif. However, instead of asserting the equality of memory accesses and program counter, it asserts the equality of an instruction counter. Its leakage model and technique are well suited against remote (non-cache) attackers.
- The tool is deployed in the CI of Amazon’s s2n library at link, where it is used to verify the time-balancedness of several parts of the codebase, handling the CBC decryption, HMAC padding, and AEAD decryption.
- Tool available: https://github.com/aws/s2n-tls/tree/main/tests/sidetrail
Themis
- Introduced in “Precise detection of side-channel vulnerabilities using quantitative cartesian hoare logic” by J. Chen, Y. Feng, and I. Dillig; https://doi.org/10.1145/3133956.3134058
- Tool not available
timecop
- Introduced in https://www.post-apocalyptic-crypto.org/timecop/
- The TIMECOP tool is a tool that uses Valgrind’s memcheck client requests
VALGRIND_MAKE_MEM_{UN}DEFINED
to essentially implement a method like ctgrind. It is a part of the SUPERCOP toolkit (System for Unified Performance Evaluation Related to Cryptographic Operations and Primitives) and is used to evaluate the constant-time properties of implementations in SUPERCOP. - Tool available: https://www.post-apocalyptic-crypto.org/timecop/
tis-ct
- http://web.archive.org/web/20200810074547/http://trust-in-soft.com/tis-ct/
- Tool not available
TriggerFlow
- Introduced in “Triggerflow: Regression Testing by Advanced Execution Path Inspection” by I. Gridin, C. P. García, N. Tuveri and B. B. Brumley; https://doi.org/10.1007/978-3-030-22038-9_16
- Tool available: https://gitlab.com/nisec/triggerflow
VirtualCert
- Introduced in “System-level non-interference for constant-time cryptography” by G. Barthe, G. Betarte, J. D. Campo, C. D. Luna, and D. Pichardie; https://doi.org/10.1145/2660267.2660283
- Tool available: https://www.fing.edu.uy/inco/grupos/gsi/project/virtualcert/