Languages Features Creators CSV Resources Challenges Add Language
GitHub icon


FaCT - Programming language

< >

FaCT is a programming language created in 2017 by Deian Stefan.

#1446on PLDB 6Years Old 126Users
0Books 1Papers

FaCT is a domain-specific language that aids you in writing constant-time code for cryptographic routines that need to be free from timing side channels. This is the compiler for the Flexible and Constant Time cryptographic programming language. 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 crypto routines from several open-source projects including OpenSSL, libsodium, and curve25519-donna. Our evaluation shows that FaCT's design makes it possible to write \emph{readable}, high-level cryptographic code, with \emph{efficient}, \emph{constant-time} behavior.

Example from the web:
void swap_conditional(secret mut uint64[5] a, secret mut uint64[5] b, secret uint64 swapi) { if (swapi == 1) { for (uint32 i from 0 to 5) { secret uint64 x = a[i]; a[i] = b[i]; b[i] = x; } } }

Publications about FaCT from Semantic Scholar

title authors year citations influentialCitations
DeFacto: Language-Parametric Fact Extraction from Source Code H. Basten and P. Klint 2009 14 1
ld-json.html 路 fact-lang.html 路 mdl.html

View source

- Build the next great programming language Search Day 215 About Blog Acknowledgements Traffic Traffic Today GitHub