TY - GEN
T1 - FACT
T2 - 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019
AU - Cauligi, Sunjay
AU - Brown, Fraser
AU - Grégoire, Benjamin
AU - Soeller, Gary
AU - Wahby, Riad S.
AU - Barthe, Gilles
AU - Stefan, Deian
AU - Johannesmeyer, Brian
AU - Renner, John
AU - Jhala, Ranjit
PY - 2019/6/8
Y1 - 2019/6/8
N2 - 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 readable, high-level cryptographic code, with efficient, constant-time behavior.
AB - 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 readable, high-level cryptographic code, with efficient, constant-time behavior.
KW - Cryptography
KW - Domain-specific language
KW - Program transformation
UR - http://www.scopus.com/inward/record.url?scp=85067688093&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85067688093&partnerID=8YFLogxK
U2 - 10.1145/3314221.3314605
DO - 10.1145/3314221.3314605
M3 - Conference contribution
AN - SCOPUS:85067688093
T3 - Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
SP - 174
EP - 189
BT - PLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation
A2 - McKinley, Kathryn S.
A2 - Fisher, Kathleen
PB - Association for Computing Machinery
Y2 - 22 June 2019 through 26 June 2019
ER -