Explore the challenges of implementing secure cryptographic algorithms and learn about FaCT, a new domain-specific language designed for constant-time programming. Delve into the complexities of writing crypto code that doesn't leak sensitive information, and discover how FaCT addresses these issues by allowing developers to use high-level language constructs while compiling to constant-time assembly. Examine the integration of FaCT into major projects like OpenSSL, libsodium, and mbedtls, as well as languages such as C, Python, and Haskell. Gain insights into timing side channels, cryptographic padding, and the intricacies of constant-time coding through practical examples. Understand the importance of labels in preventing information leakage, the automatic code transformations performed by FaCT, and the verification process for constant-time code. Analyze performance metrics and user study results, and consider future directions for this innovative approach to cryptographic programming.
Overview
Syllabus
Intro
Timing side channels
Cryptographic padding
Constant-time coding example
Padding removal: 1st try
Writing constant-time code is hard
Error-prone in practice
What does Fact look like?
Labels ensure no leakage
Automatically transform code
Transformations are tricky
Verifying constant-time code
Interoperate with external code
Performance numbers
User study results
Future directions
Taught by
Strange Loop Conference
