FACT: A DSL for timing-sensitive computation

Sunjay Cauligi, Fraser Brown, Benjamin Grégoire, Gary Soeller, Riad S. Wahby, Gilles Barthe, Deian Stefan, Brian Johannesmeyer, John Renner, Ranjit Jhala

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

Abstract

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.

Original languageEnglish
Title of host publicationPLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation
EditorsKathryn S. McKinley, Kathleen Fisher
PublisherAssociation for Computing Machinery
Pages174-189
Number of pages16
ISBN (Electronic)9781450367127
DOIs
Publication statusPublished - 8 Jun 2019
Externally publishedYes
Event40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019 - Phoenix, United States
Duration: 22 Jun 201926 Jun 2019

Publication series

NameProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)

Conference

Conference40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019
Country/TerritoryUnited States
CityPhoenix
Period22/06/1926/06/19

Funding

We thank the anonymous PLDI and PLDI AEC reviewers and our shepherd Limin Jia for their suggestions and insightful comments. We thank the participants of the Dagstuhl Seminar on Secure Compilation for early feedback on this work, especially Tamara Rezk. We thank Ariana Mirian for handling the IRB for our user study, Shravan Narayan for his help in understanding the subtleties of LLVM, and Joseph Jaeger and Jess Sorrell for helping us understand elliptic curve implementations. We also thank the CSE 130 TAs for their help in testing our user study, and the CSE 130 students for participating in the user study. This work was supported in part by gifts from Fujitsu and Cisco, by the National Science Foundation under Grant Number CNS-1514435, by ONR Grant N000141512750, and by the CONIX Research Center, one of six centers in JUMP, a Semiconductor Research Corporation (SRC) program sponsored by DARPA.

FundersFunder number
National Science Foundation1514435, CNS-1514435, N000141512750

    Keywords

    • Cryptography
    • Domain-specific language
    • Program transformation

    Fingerprint

    Dive into the research topics of 'FACT: A DSL for timing-sensitive computation'. Together they form a unique fingerprint.

    Cite this