5 posts tagged “High-Assurance Cryptography”.
Five proof-of-concept exploits against ML-DSA, ML-KEM, Ed25519, and ChaCha20 demonstrate three classes of semantic gap in hax's Rust-to-F* extraction pipeline, where verified models diverge from deployed code.
11 min readAn examination of CE Labs' TLS implementations reveals 75% of valid ECDSA signatures rejected, authentication tags silently dropped, no certificate validation, and remote denial-of-service vectors.
11 min readThree 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.
12 min readCE Labs said they'd be 'very interested' if someone found a bug in their verified code. We found three.
13 min readA case study on CE Labs' libcrux exposing the gap between formal verification marketing and engineering reality.
10 min read