FaCT: A New Language for Constant-Time Programming
summary
FaCT is a domain specific language that compiles high-level code into constant-time assembly and embeds into C Python and Haskell toolchains. It rejects secret-indexing and recursion, transforms branches into branch-free CT selects, and uses z3 and CT-vera to prove post‑transformation memory safety and constant time. Ports of OpenSSL libsodium and mbedtls show performance near C and sometimes faster (libsodium vector ops). A user study finds programmers understand and write FaCT code more reliably than hand‑rolled constant‑time C. Source lives on GitHub.
AI-written summary · about
chapters (16)
- 0:00Intro
- 0:24Timing side channels
- 1:38Cryptographic padding
- 2:10Constant-time coding example
- 2:45Padding removal: 1st try
- 8:21Writing constant-time code is hard
- 8:46Error-prone in practice
- 11:08What does Fact look like?
- 12:17Labels ensure no leakage
- 14:16Automatically transform code
- 17:10Transformations are tricky
- 18:06Verifying constant-time code
- 19:06Interoperate with external code
- 20:28Performance numbers
- 22:15User study results
- 23:52Future directions
related talks
32mVerifying Constant-Time Implementations
28mType-directed Program Transformation for Constant-Time Enforcement
23mRobust Constant-Time Cryptography
24mA CompCert Compiler that Preserves Cryptographic Constant-time
26mType-directed Program Transformation for Constant-Time Enforcement
18mPreservation of Speculative Constant-time by Compilation
23mSmooth, Integrated Proofs of Cryptographic Constant Time for Nondeterministic Programs(…)
17mRobust Constant-Time Cryptography