A blueprint for formal verification of Apple corecrypto
7 hours ago
- #Apple security
- #quantum cryptography
- #formal verification
- Apple has introduced quantum-secure cryptography in iMessage to protect users from future quantum computer threats.
- They have deployed ML-KEM and ML-DSA algorithms, following NIST standards (FIPS 203 and FIPS 204), in their corecrypto library.
- A rigorous formal verification process was developed to ensure mathematical correctness of implementations.
- The approach combines tools like Isabelle, SAW, and Cryptol, with custom methods for verifying both C and ARM64 assembly code.
- Formal verification caught subtle bugs not detectable by conventional testing, enhancing security assurance.
- The corecrypto library is foundational, used across 2.5 billion Apple devices for encryption, hashing, and signatures.
- New algorithms are included based on strict criteria: security improvement, secure design, high performance, and compact parameters.
- Implementations must be secure, optimized, and correct, with hand-tuned optimizations for Apple silicon.
- Apple has released their formal verification tools and methodologies publicly to advance industry standards.
- The work emphasizes combining formal verification with conventional testing for the strongest security assurance.