Room 1.2
Invited Talk Parallel session Formal Verification
The Formosa-Crypto Approach to Formally Verified Cryptography
Manuel Barbosa (University of Porto (FCUP) & INESC TEC & PQShield, Associate Professor)
In this talk I will provide an overview of the formosa-crypto formal verification framework, covering both Jasmin and EasyCrypt, and explaining the tradeoffs that they offer. This will include a description of the methodology, explaining what is proved, in which tool, what effort this involves and how it all comes together to give a formal meaning to the security of low-level code.
I will also provide some motivation on why formal verification matters in the post-quantum migration and summarize the status of the formosa-crypto work in this area, focusing on the post-quantum standards ML-KEM, ML-DSA and SLH-DSA.