Metadata
| Year | 2019 |
|---|---|
| Target | LLVM IR |
| Technique | Symbolic |
| Guarantees | sound with restrictions |
| Available | yes |
| Repository | https://github.com/PLSysSec/haybale-pitchfork |
| Tutorial | yes |
Abstract
pitchfork is a tool for verifying that constant-time code is, indeed, constant-time. It can analyze code written in C/C++, Rust, or any other language which can compile to LLVM bitcode (e.g., Swift, Go, and others). Given a function to analyze, pitchfork will either report that the function is constant-time, or give a detailed explanation of why it is not, including the line number of the constant-time violation in the original source, full sequence of branch decisions leading to the violation, and values of all variables at the point of the violation.
pitchfork is built on the haybale symbolic execution engine, which is also written in Rust.