Security Announcement: Bugs in Noise Explorer's Rust/WASM Code Generation
We've updated Noise Explorer to address two bugs in generated Rust and WebAssembly implementations of Noise Protocol Framework handshake patterns.
2 min readFrom the blog.
Insights on cryptography, security research, and software engineering from Symbolic Software.
-
-
Even More Bugs in Cryspen's libcrux: ML-DSA
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.
13 min read -
We Found Bugs in Cryspen's Verified Code
Cryspen said they'd be 'very interested' if someone found a bug in their verified code. We found three.
12 min read -
Verifpal Verifies Signal Across Three Messages
Verifpal 0.31.2 ships a major overhaul to active attacker analysis, finally enabling full verification of Signal's three-message protocol.
7 min read -
Drain Brain: Symbolic Software's Latest Puzzle Game!
A rigorous defense of publishing puzzle games from an applied cryptography consultancy, requiring no defense.
2 min read -
On the Promises of 'High-Assurance' Cryptography
A case study on Cryspen's libcrux exposing the gap between formal verification marketing and engineering reality.
10 min read