Apple Releases Quantum-Resistant Cryptography Code and Verification Tools
Summary
Apple released ML-KEM and ML-DSA implementations in corecrypto, plus formal verification tools and documentation. Apple says verification uncovered a missing ML-DSA step that could have silently broken digital signatures if it had reached production.
Key points
- Apple made its ML-KEM and ML-DSA implementations in corecrypto, along with verification tools, libraries, and methodology documentation, publicly available.
- The release includes a Cryptol-to-Isabelle translator and supporting materials to reproduce the formal verification results.
- Apple says verification found a missing computational step in ML-DSA that could have silently broken digital signatures if the bug had reached production.
- Apple began deploying quantum-resistant encryption in iMessage in 2024 and has expanded it to VPN services and TLS networking protocols.
- Apple says it combines formal verification with conventional testing because its tools could not verify every aspect of the code.
Article Details
- Event Type
- Open-source release of quantum-resistant cryptographic implementations and formal-verification tooling
- Impact
- Apple’s verification process found a missing computational step in the ML-DSA code that could have silently broken digital signatures. If the bug had reached production, iMessage messages might have appeared authenticated despite lacking proper security, leaving users unaware. Apple made the implementations and verification tools available for independent review and broader industry use.
Vendors
Products
corecryptoThe release covers ML-KEM and ML-DSA in corecrypto, and Apple says its hybrid verification approach uncovered a bug that conventional testing could have missed.iMessageApple began deploying quantum-resistant encryption in iMessage in 2024 and has expanded the technology to VPN services and TLS networking protocols.