Chelpis QSMC Online Talk: Formosa crypto -- high-assurance crypto in practice

Implementations of cryptography are currently facing new challenges in multiple dimensions. New cryptosystems that resist attacks even by future adversaries equipped with a large universal quantum computer are being deployed and they are much more complex to implement and analyze than today's elliptic-curve cryptography. At the same time, even side-channel attackers who are constrained to software-visible leakage are becoming increasingly powerful: attacks based on transient execution have demonstrated that the traditional "constant-time" programming paradigm for protecting cryptographic software against software-side-channels is insufficient. Furthermore, compilers for mainstream programming languages like C and Rust incorporate more and more optimizations that break carefully crafted source-level security mechanisms. In my talk I will present the Formosa Project -- an ambitious effort aiming at building and deploying high-assurance post-quantum crypto software. I show how a new generation of tools is able to tackle the complexity that we are facing for the next generation of cryptographic software and how these tools are able to give very strong guarantees about correctness, cryptographic security, and implementation security.