Usuba: High-Throughput and Constant-Time Ciphers, by Construction
Cryptographic primitives are subject to diverging imperatives. Functional correctness and auditability pushes for the use of a high-level programming language. Performance and the threat of timing attacks push for using no more abstract than an assembler to exploit (or avoid!) the micro-architectural features of a given machine. We believe that a suitable programming language can reconcile both views and actually improve on the state of the art of both. Usuba is an opinionated dataflow programming language in which block ciphers become so simple as to be “obviously correct” and whose types document and enforce valid parallelization strategies at the granularity of individual bits. Its optimizing compiler, Usubac, produces high-throughput, constant-time implementations performing on par with hand-tuned reference implementations. The cornerstone of our approach is a systematization and generalization of bitslicing, an implementation trick frequently used by cryptographers.
Mon 24 Jun
|10:00 - 10:20|
Roshan DathathriUniversity of Texas at Austin, USA, Olli Saarikivi, Hao ChenMicrosoft Research, Kim LaineMicrosoft Research, n.n., Kristin LauterMicrosoft Research, n.n., Saeed MalekiMicrosoft Research, Madan MusuvathiMicrosoft Research, Todd MytkowiczMicrosoft ResearchDOI Pre-print Media Attached
|10:20 - 10:40|
|10:40 - 11:00|
Sunjay CauligiUniversity of California, San Diego, Gary Soeller, Brian JohannesmeyerUniversity of California at San Diego, USA, Fraser BrownStanford University, Riad S. WahbyStanford University, USA, John RennerUniversity of California, San Diego, Benjamin GregoireINRIA, Gilles BartheIMDEA Software Institute, Ranjit JhalaUniversity of California, San Diego, Deian StefanUniversity of California San DiegoMedia Attached