| Website | https://www.cryspen.com/ |
| Github | https://github.com/cryspen |
Thrilled to welcome @blement to Cryspen's Tools and Proofs team! ๐ Clรฉment's expertise in formal methods (PhD from Inria Paris!) will be for conducting rigorous proofs and enhancing our tooling. Welcome, Clรฉment! ๐
MLS Group State Forks: What, Why, How
Group state forks are faulty states that MLS groups can end up in. We have a new blog post that looks at what they are exactly, how that happens and how to resolve them. We also look at a new OpenMLS feature that makes fork resolutions a little easier.
Get all the details on our blog: https://cryspen.com/post/mls-fork-resolution/
Rust identifiers, demystified! We're revealing our analysis toolchain's secrets in our latest blog. Discover how we tackle global vs. local identifiers for better formal verification with hax.
Read the full story: https://hax.cryspen.com/blog/2025/04/01/redesigning-global-identifiers-in-hax/
Updates from some of Cryspen's Open Source Projects!
Check out our latest updates:
- Dive into the latest developments from the past month on ๐ก๐๐ฑ. https://hax.cryspen.com/blog/2025/04/01/this-month-in-hax-march-2025/
- And see how the ๐๐ฉ๐๐ง๐๐๐ project is progressing and what's on the horizon. https://blog.openmls.tech/posts/2025-04-01-this-month-in-openmls/
Real World Crypto 2025 buzzed with energy as the cutting edge of cryptography was presented to and discussed among an audience of leading researchers and developers from academia and industry. Today, on the second day of the conference, Cryspen teamed up with Google to showcase practical, scalable, verified solutions for high-assurance software and post-quantum cryptography.
New blog post! ๐ Control flow analysis with Hax. In this post we show how to ensure control flow properties such as "function A is always called before function B" in Rust. Super relevant for security! ๐
๐ hax is entering a new era! ๐
We're excited to announce the launch of our new website, a fresh start at Cryspen, and our first official release, v0.1.0!
Check out our latest blog post to learn more about this exciting new chapter and how you can get involved.
๐ https://hax.cryspen.com/blog/2025/01/21/a-new-chapter.html
#opensource #hax
Are you ready for the post-quantum era?
Test your PQC readiness now! Our new website, featuring our formally verified libcrux crypto library, makes it easy to see if your browser is future-proof.
Head over to https://buff.ly/4ak1LB6 to test your browser and learn more about post-quantum cryptography.
Great News! Cryspen's libcrux crypto library was mentioned in a recent article in The Register that discusses a new method for converting C code to Rust.
We're proud that libcrux is being recognized here. If you're interested in learning more about libcrux, or how it can be used to improve the security of your applications, please visit our website or contact us today.
When implementing cryptographic protocols, ensuring input validation is paramount. Neglecting this can lead to severe vulnerabilities, including information leakage, state corruption, and impersonation attacks.
In a recent blog post, Jan delved into how we address input validation in OpenMLS, an open-source Rust implementation of the Messaging Layer Security (MLS) protocol.
https://blog.openmls.tech/posts/2024-09-30-taking-stock-of-validation-checks/
When implementing cryptographic protocols, probably the most important thing is to not forget validating all inputs. Failing to do so can lead to inadvertant leakage of private information, state corruption, impersonation attacksโฆ all kinds of vulnerabilities. To give an example, you might remember the โgoto failโ vulnerability, a bug in the TLS implementation used in iOS. Here, the verification function of signatures sent along with the ServerKeyExchange message, which ties the server identity to the transcript and ephemeral key material. Due to a hard-to-spot slipup, it returned success early and never really checked the signature, which would allow an attacker to man-in-the-middle the connection. While in this case they didnโt just forget to do the check, it does demonstrate why these checks are important.
