top of page

Online Talk -
Formosa crypto -- high-assurance crypto in practice

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.

[Date & Time]

  • Date: Feb 20, 2024 (Tue)

  • Time: 15:00-16:00 UTC+8

  • Location: Online


Peter Schwabe is research group leader at MPI-SP and professor at Radboud University. He graduated from RWTH Aachen University in computer science in 2006 and received a Ph.D. from the Faculty of Mathematics and Computer Science of Eindhoven University of Technology in 2011. He then worked as a postdoctoral researcher at the Institute for Information Science and the Research Center for Information Technology Innovation of Academia Sinica, Taiwan and at National Taiwan University. His research area is cryptographic engineering; in particular the security and performance of cryptographic software. He published more than 60 articles in journals and at international conferences presenting, for example, fast software for a variety of cryptographic primitives including AES, hash functions, elliptic-curve cryptography, and cryptographic pairings. He has also published articles on fast cryptanalysis, in particular attacks on the discrete-logarithm problem. In recent years he has focused in particular on post-quantum cryptography. He co-authored the "NewHope" and "NTRU-HRSS" lattice-based key-encapsulation schemes which were used in post-quantum TLS experiments by Google and he is co-submitter of seven proposals to the NIST post-quantum crypto project, all of which made it to the second round, five of which made it to the third round, and 3 of which were selected after round 3 for standardization.In 2021, he co-founded the Formosa-Crypto project, an effort by multiple research groups to build (post-quantum) cryptographic software with formal proofs of functional correctness and security.


 [Register Here]

bottom of page