Let's Chat
Insights on cryptography, security research, and software engineering from Symbolic Software.
Three findings in libcrux's ML-DSA implementation: a verifier norm check that is dead code due to a wrong constant, a missing bounds check in hint deserialization, and a wrong multiplication specification that renders AVX2 proofs unsound.
Cryspen said they'd be 'very interested' if someone found a bug in their verified code. We found three.
Verifpal 0.31.2 ships a major overhaul to active attacker analysis, finally enabling full verification of Signal's three-message protocol.
A rigorous defense of publishing puzzle games from an applied cryptography consultancy, requiring no defense.
A case study on Cryspen's libcrux exposing the gap between formal verification marketing and engineering reality.
We're thrilled to announce Cedarcrypt, a new applied cryptography summer school and conference.