Apple Verifies Quantum-Secure Crypto in corecrypto

Apple Publishes Quantum-Secure Cryptography in corecrypto

The release of corecrypto includes Apple’s implementations of the quantum-secure ML-KEM (Key Encapsulation Mechanism) and ML-DSA (Digital Signature Algorithm) algorithms. These algorithms, standardized by NIST as FIPS 203 and FIPS 204, respectively, represent the forefront of post-quantum cryptography. Apple states it is publishing these implementations, along with their associated mathematical proofs, for independent evaluation by security experts.

Furthermore, Apple has open-sourced the formal verification libraries and tools developed for this initiative. This public release aims to advance the state of the art for assuring critical software, providing the strongest known correctness results for any widely-deployed production implementation of these algorithms. The corecrypto source archive is available for review, allowing the broader security community to examine the underlying code. corecrypto source archive

Addressing the Quantum Threat Across Apple Platforms

Apple began its transition to quantum-secure cryptography with its introduction in iMessage, recognizing the well-documented threat from future quantum computers. The company has since expanded this deployment to other critical areas, including VPN and TLS networking, where sensitive information is frequently exchanged. Additionally, quantum-secure APIs were included with the Apple CryptoKit release last fall, empowering developers to integrate these advanced encryption and authentication methods into their own applications. Apple CryptoKit

Given that corecrypto underpins encryption, decryption, hashing, random number generation, and digital signatures across over 2.5 billion active Apple devices, any vulnerability could compromise numerous apps and features. Apple employs a stringent set of criteria for including new algorithms. These include improving security, possessing a secure theoretical design, demonstrating high performance across all Apple devices, and maintaining compact parameters for key sizes, signatures, and ciphertexts.

Rigorous Formal Verification Ensures Implementation Correctness

To meet its high standards, Apple has implemented rigorous formal verification methods to prove the mathematical correctness of its quantum-secure implementations. This approach involves using mathematical proofs to demonstrate that an algorithm satisfies predefined properties, offering a significantly higher degree of assurance than conventional software testing. Apple has utilized formal verification in silicon development for over 15 years and applied it to classical cryptography, including the hardware Public Key Accelerator (PKA).

The company developed a custom approach for corecrypto’s formal verification, combining existing tools like Isabelle, a powerful proof assistant, with new ones such as Software Analysis Workbench (SAW) and Cryptol. A specialized Cryptol-to-Isabelle translator, developed with Galois, helps bridge the gap between different language models. This process involves translating the C implementation into Cryptol, verifying it with SAW, then translating the Cryptol model into Isabelle to prove its equivalence against the manually translated FIPS specifications. This meticulous, multi-step process, involving over 50,000 proof steps and new Isabelle theories, addresses the complexities of ML-KEM and ML-DSA, ensuring functional correctness and security.

A Proactive Stance on Next-Generation Cryptographic Security

Apple’s proactive adoption and formal verification of quantum-secure cryptography in corecrypto underscore its commitment to user security in an evolving threat landscape. By not only deploying these advanced algorithms but also publishing its methods and tools, Apple contributes significantly to the broader cryptographic community. This initiative sets a high bar for the secure implementation of post-quantum standards, mitigating potential vulnerabilities before quantum computers become a practical threat.