From f8163bd3202c12a715a9b70c2b5163e3aa9d3220 Mon Sep 17 00:00:00 2001 From: Franziskus Kiefer Date: Mon, 19 Aug 2024 11:55:52 +0200 Subject: [PATCH] rebuilding site Mon Aug 19 11:55:52 CEST 2024 --- post/fospqc/index.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/post/fospqc/index.html b/post/fospqc/index.html index 03c0880..a0f2c09 100644 --- a/post/fospqc/index.html +++ b/post/fospqc/index.html @@ -260,7 +260,7 @@

Formally Verified Po

At Cryspen, we have been developing formally verified open-source implementations of post-quantum cryptographic algorithms in Rust using the hax toolchain. Our implementations are verified to be panic free, functionally correct, and secret independent. Indeed, our verification of Kyber already uncovered vulnerabilities that were found to be present and exploitable in multiple Kyber implementations.

We have been working with Mozilla to upstream our verified implementations into the NSS cryptographic library. We are also contributing our Rust code to the PQCP project hosted by the Post Quantum Crypto Alliance.

-

And now, we are happy to announce that we are also partnering with Google to develop formally verified open-source implementations of the NIST standards that can be consumed not only by organizations like Google, but by anyone needing to embrace the imminent PQC transition.

+

And now, we are happy to announce that we are also partnering with Google to develop formally verified open-source implementations of the NIST standards that can be consumed not only by organizations like Google, but by anyone needing to embrace the imminent PQC transition.

Cryspen provides open source high-performance, high-assurance implementations of ML-KEM (FIPS 203) and ML-DSA (FIPS 204). They will be available as Rust crates, as well as C code packages. Other versions, including those optimized for IoT devices, can be licensed on request.