CONIX Publication

FaCT: A DSL for Timing-Sensitive Computation

Authors: Sunjay Cauligi, Gary Soeller, John Renner, Deian Stefan, Fraser Brown, Brian Johannesmeyer, Riad S. Wahby, Gilles Barth, Benjamin Gregoire, Ranjit Jhala


Real-world cryptographic code is often written in a subset of C intended to execute in constant time, thereby avoiding timing side channel vulnerabilities. This C subset eschews structured programming as we know it: if-statements, looping constructs, and procedural abstractions can leak timing information when handling sensitive data. The resulting obfuscation has led to subtle bugs, even in widely-used high-profile libraries like OpenSSL. To address the challenge of writing constant-time cryptographic code, we present FaCT, a crypto DSL that provides high-level but safe language constructs. The FaCT compiler uses a secrecy type system to automatically transform potentially timing-sensitive high-level code into low-level, constant-time LLVM bitcode. We develop the language and type system, formalize the constant-time transformation, and present an empirical evaluation that uses FaCT to implement core cryptographic routines from several open-source projects including OpenSSL, libsodium, and curve25519-donna. Our evaluation shows that FaCT's design makes it possible to write _readable., high-level cryptographic code, with _efficient_, _constant-time_ behavior.

Release Date: 06/22/2019
Uploaded File: View