A blueprint for formal verification of Apple corecrypto
A blueprint for formal verification of Apple corecrypto
Apple corecrypto 形式化验证蓝图
The 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. iMessage 中量子安全加密技术的引入，标志着一项重大安全转型的开始，旨在保护 Apple 用户免受未来量子计算机带来的威胁。在所有 Apple 平台上大规模部署这一代新算法需要极高的可靠性，因此我们开发了严谨的新型形式化验证方法，以证明我们实现的数学正确性。
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. 随着本周 corecrypto 的发布，我们公开了量子安全 ML-KEM 和 ML-DSA 算法的实现，以及我们为确保其符合 FIPS 203 和 FIPS 204 标准而构建的数学证明，供专家进行独立评估。为了进一步推动关键软件保障技术的进步，我们还发布了形式化验证库和工具，这些工具使我们能够为相关算法的任何广泛部署的生产实现，实现目前已知最强的正确性验证结果。
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. 2024 年，我们将后量子加密技术添加到了 Apple 操作系统基础加密库 corecrypto 中。为了应对未来量子计算机带来的明确威胁，我们致力于首先在最能发挥作用的领域开发和部署强大的量子安全加密技术，这些领域包括涉及加密通信和其他敏感信息的应用，如 iMessage、VPN 和 TLS 网络。此外，去年秋季随 Apple CryptoKit 发布的量子安全 API，使开发者能够在自己的应用中采用量子安全加密和身份验证。
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. corecrypto 在我们的产品中被持续使用，为超过 25 亿台活跃设备提供加密、解密、哈希、随机数生成和数字签名功能。corecrypto 中的一个关键漏洞可能会危及所有依赖它的应用和功能的安全性与可靠性，因此我们在向库中添加新代码时非常谨慎，并竭尽全力进行全面测试。
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. 我们仅在通过以下标准的全面评估后，才会将新的加密算法纳入 corecrypto：提升安全性。算法必须能解决新问题或改进现有算法的安全性。安全设计。算法必须具备强大的理论安全性，并经受住全球研究界严谨且持续的密码分析。在实践中，必须能够以安全的方式实现该算法以满足我们的预期用途。高性能。在所有 Apple 设备上实现时，执行效率必须极高（包括延迟和功耗方面）。紧凑的参数。密钥大小、签名和密文必须最大限度地减少对网络延迟的影响，并符合设备的内存限制。
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. 当算法达到我们纳入 corecrypto 的高标准时，我们开发的实现必须满足：安全。代码必须符合严格的安全标准，且不得泄露信息。这既需要正确性，也需要加固，例如防止泄露攻击者可能用于提取应用机密的计时信号。优化。实现应最大限度地利用其运行所在的芯片指令集和架构。正确。代码（包括所有相关优化）必须忠实地实现密码学界所分析的标准中定义的算法，并产生正确的输出。
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. 在评估纳入 corecrypto 的量子安全算法时，我们很快确定了两种符合我们标准的算法——这两种算法后来也被 NIST 选中并标准化为 ML-KEM 和 ML-DSA（分别为 FIPS 203 和 FIPS 204）。虽然 NIST 也标准化了其他签名方案，但 ML-KEM 和 ML-DSA 最符合我们的要求。密码学界的大量工作已经为 ML-KEM 和 ML-DSA 提供了参考实现，根据我们的评估，这些实现展现了强大的安全性和性能基础。
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. 由于 corecrypto 被用于各种 Apple 产品（包括具有不同微架构的专用芯片），我们首先使用可移植的 C 代码编写算法实现。为确保实现能够在部署 corecrypto 的任何地方正确且安全地运行，我们的准则非常严格：我们编写代码以避免通过执行计时泄露机密值，防止编译器无意中削弱这些保护措施，并利用 Apple 处理器上的数据独立计时 (DIT) 和指针身份验证 (PAC) 等硬件特性，分别防范一系列微架构侧信道攻击，并针对内存损坏漏洞进行加固。此外，我们还会根据特定用途的威胁模型评估是否需要对内部计算进行随机化处理。
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. 在审查了 ML-KEM 和 ML-DSA 设计随附的参考实现后，我们发现了进一步改进的重大机会。我们应用了数学优化，在不改变底层算法的情况下提高了性能，并仔细重写了对性能和安全性最敏感的子程序，以充分利用我们行业领先的处理器。凭借我们在 Apple 芯片方面的深厚专业知识，这些手动优化的路径还使我们能够精确控制处理器行为，从而帮助防止可能向攻击者泄露机密的计时侧信道攻击。
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. 引入这些复杂算法的新实现并融入我们的重大改进是一项艰巨的任务。更具挑战性的是，ML-KEM 和 ML-DSA 底层的数学原理本身相对较新，因此业界在将这些算法安全地实现到出货产品中的集体经验要少得多。在每一步中，我们都深感有必要避免业界在早期部署椭圆曲线加密技术时所经历的问题。