A blueprint for formal verification of Apple corecrypto - Apple Security Research

Written by Apple Security Engineering and Architecture (SEAR) and Hardware Technologies Formal VerificationThe introduction of quantum-secure cryptography in iMessage marked the start of a significant security transition to protect Apple users from threats posed by future quantum computers. Deploying this new generation of algorithms at scale across all Apple platforms requires high assurance, so we developed rigorous new formal verification methods to prove the mathematical correctness of our implementation. With this week’s release of corecrypto, we’re publishing our implementations of quantum-secure ML-KEM and ML-DSA algorithms — along with the mathematical proofs we built to assure they are faithful to the FIPS 203 and FIPS 204 specifications — for independent evaluation by experts. And to further advance the state of the art for assuring critical software, we're also publishing the formal verification libraries and tools that we created to achieve the strongest known correctness results for any widely-deployed production implementation of the relevant algorithms.

In 2024, we added post-quantum encryption to corecrypto, the foundational cryptographic library in Apple operating systems. To address the well-documented threat from future quantum computers, we’ve been working to first develop and deploy strong, quantum-secure cryptography in areas where it’s likely to have the greatest benefit: applications involving encrypted communications and other sensitive information, including iMessage, VPN, and TLS networking. In addition, quantum-secure APIs included with our Apple CryptoKit release last fall enable developers to adopt quantum-secure encryption and authentication in their own apps. corecrypto is used continuously in our products, providing encryption and decryption, hashing, random number generation, and digital signatures on over 2.5 billion active devices. A critical bug in corecrypto has the potential to compromise the security and reliability of every app and feature that depends on it, so we are conservative when adding new code to the library and make exceptional efforts to be comprehensive in our testing. We include new cryptographic algorithms in corecrypto only after a thorough assessment against the following criteria:

Improves security. The algorithm must solve new problems or improve on the security of existing algorithms. Secure design. The algorithm must have strong theoretical security, and must have withstood rigorous, sustained cryptanalysis from the global research community. And practically, it must be feasible to implement the algorithm in a secure way for our intended use.

High performance. Execution must be highly efficient — both in terms of latency and power — as implemented across every Apple device. Compact parameters. Key sizes, signatures, and ciphertexts must minimize their impact on network latency and fit within device memory constraints.

When an algorithm meets our high bar for inclusion in corecrypto, we develop an implementation that must then be:

Secure. The code must meet exacting security criteria and must not leak information. This requires both correctness and hardening, such as to prevent leaking timing signals that an adversary could use to extract application secrets. Optimized. The implementation should take maximum advantage of the instructions and architecture of the silicon on which it runs. Correct. The code, including all relevant optimizations, must faithfully implement the algorithm as defined in the standard which was analyzed by the cryptographic community. It must produce the correct output.

When we evaluated quantum-secure algorithms to include in corecrypto, we quickly converged on two that met our criteria — the same two that would later be selected and standardized by NIST as ML-KEM and ML-DSA (FIPS 203 and FIPS 204, respectively). While NIST also standardized other signature schemes, ML-KEM and ML-DSA best matched our requirements. Significant work by the cryptographic community had produced reference implementations for ML-KEM and ML-DSA that, in our own evaluation, showed a strong foundation of security and performance. Because corecrypto is used across Apple products — including specialized chips with different microarchitectures — we start by writing our algorithm implementations in portable C code. To ensure the implementations run correctly and securely wherever corecrypto is deployed, our guidelines are strict: we write this code to avoid leaking secret values through execution timing, prevent the compiler from inadvertently weakening those protections, and take advantage of hardware features like Data Independent Timing (DIT) and Pointer Authentication (PAC) on Apple processors, which respectively guard against a range of micro-architectural side channels and harden against memory corruption exploits. In addition, we evaluate the need to randomize internal computations based on use-specific threat models. After reviewing the reference implementations accompanying the ML-KEM and ML-DSA design, we identified significant opportunities for further improvement. We applied mathematical optimizations that increase performance without changing the underlying algorithms, and we carefully rewrote the most performance- and security-sensitive subroutines to take full advantage of our industry-leading processors.

Drawing on our deep expertise with Apple silicon, these hand-optimized paths also give us precise control over processor behavior to help prevent the kind of timing side channels that could expose secrets to an attacker. It’s a significant undertaking to introduce novel implementations of these complex algorithms that incorporate our substantial improvements. Making matters more challenging, the mathematics underlying ML-KEM and ML-DSA is itself relatively recent, so there is much less collective experience in the industry implementing these algorithms securely in shipping products. At every step, we were deeply motivated to avoid issues that the industry previously experienced with early deployments of elliptic curve cryptography, which were hindered by subtle and exploitable bugs. Our top priority was to ensure that the new algorithm implementations, with our hand-tuned optimizations for performance and security hardening, are functionally correct and secure. To meet this goal, we set an exceptional qualification threshold that includes deep conventional testing, simulation, and independent review, and combines it with rigorous formal verification. Our formal verification requirements Formal verification uses mathematical proofs to demonstrate that a system or object satisfies specific properties that we define. At Apple, we've performed extensive formal verification in silicon development for over 15 years, and in 2019 we began using formal verification to prove classical cryptography, including the hardware Public Key Accelerator (PKA) — the part of Apple silicon that performs elliptic curve public key operations. For corecrypto, we use mathematical proofs to show that our algorithm implementations are correct to a significantly greater degree of assurance than conventional software testing allows. Put simply: if we can prove that the mathematical formula of our implementation is equivalent to that of its specification, then we know that our implementation will produce the correct output. In theory, this gives us strong assurance that our implementation will work correctly every time. Such a high degree of assurance generally cannot be obtained through conventional testing. The practical considerations are more complicated. Regardless of how it’s applied, formal verification requires a tremendous investment of time and deep expertise. The implementation and its specification must be represented with carefully chosen mathematical formulas. To draw correct conclusions, the formulas must correctly model the relevant behaviors of both the implementation and the specification, and be structured so as to enable the proof to be written in simple steps. The formulas must also be complete enough to cover all the inputs we require.

Since the resulting formulas can be extremely large, it takes specialized engineering skill — including a profound understanding of the underlying mathematics — to write the mathematical proofs, and to master the tools used to verify those proofs step by step. It often takes many iterations to successfully construct a proof strategy for verification. By analyzing how we might best combine formal verification for ML-KEM and ML-DSA with our existing engineering processes, we developed the key requirements for formal verification of corecrypto. In practice, our selected algorithms have several functions: key generation, encapsulation, and decapsulation in ML-KEM, and key generation, signature generation, and signature verification for ML-DSA. Each of these functions is implemented by a sequence of specialized subroutines that is traditionally prone to subtle arithmetic bugs, especially for large operands such as polynomials and big numbers. These subroutines usually involve carries or borrows during computation, which the implementation needs to handle correctly but which are too numerous and too deep in the sequence of subroutines to be thoroughly checked with conventional tests. Formal verification can help demonstrate that each of these subroutines produces the correct output on specified inputs. But verifying each subroutine individually is not sufficient, because optimized subroutines may represent objects in slightly different ways, and bugs can be missed if the output of a subroutine is not shown to be fully compatible with the next one in the sequence, such as when the output value of an intermediate subroutine falls outside of the range of inputs supported by the next subroutine. These details helped shape our key requirements for formal verification of Apple corecrypto:

Our formal verification must be capable of verifying our entire algorithm implementation, including our advanced mathematical formulas. It must be able to demonstrate that each subroutine individually produces the correct output, and that the full sequence of subroutines together computes the correct final result. To account for the wide range of products that use corecrypto, our verification must support algorithm implementations that are written in portable C and in ARM64 assembly, the instruction language used by Apple silicon. Because we continuously evolve our software to improve our implementation and support new applications, our verification must support rapid evolution and minimize the effort required to keep our correctness proof valid, including maintaining compatibility with our existing developer tools.

A custom approach for corecrypto To find the right approach, we evaluated a number of verification tools and existing verified implementations.