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
CountryUnited States
CityPhoenix
Period22/06/1926/06/19

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