Cryptographic mechanisms are crucial to the security of our digital lives but their design and implementation remains notoriously difficult and error-prone. With the help of two ERC Grants, Karthikeyan Bhargavan and the Prosecco team at Inria have developed state-of-the-art formal verification techniques that can be applied to real-world cryptographic software. In particular, they used these techniques to help design and analyze the TLS 1.3 protocol standard, as well to build the HACL* verified cryptographic library, code from which has been incorporated in mainstream software projects including Mozilla Firefox, the Linux Kernel, the Tezos Blockchain, the WireGuard VPN, and the ElectionGuard voting system.
The goal of this new ERC Proof of Concept grant is to build upon these these landmark research results and to commercialise the associated know-how through a new company called Cryspen. Cryspen will build a verified cryptographic software stack and an associated verification toolchain that is well-documented and easy to use for security developers. Cryspen will offer consulting and support contracts for this stack as well as software contracts for developing new cryptographic applications, ranging from secure messaging system to privacy-preserving machine learning.
Cryspen is co-founded by Franziskus Kiefer (CEO), Karthikeyan Bhargavan, and Jonathan Protzenko. For more information, email email@example.com