Apple在GitHub上发布iPhone与Mac后量子密码学代码

苹果公司今日在GitHub上公开了全新的corecrypto源代码，并发布了一篇详尽的技术文章，深入介绍其在iPhone、Mac等产品上推进后量子密码学工作的具体细节。

苹果此次在GitHub上发布了全新的corecrypto代码仓库，这是其后量子密码学工作更大范围更新的一部分。该项工作自2024年起随iMessage的PQ3协议正式向公众推出。

PQ3协议随iOS 17.4一同发布，是苹果在后量子保护领域迈出的第一个重要公开步骤，旨在保护用户免受未来量子计算机的威胁。iMessage通过PQ3在会话启动时以及加密密钥定期刷新时均提供后量子级别的保护。

此次发布延续了上述工作。GitHub代码仓库包含corecrypto的源代码，这是苹果安全框架、CryptoKit以及CommonCrypto底层所使用的密码学库，负责支撑加密、哈希、随机数生成以及数字签名等核心功能。

代码仓库中还包含苹果为corecrypto选定的两种后量子算法——ML-KEM与ML-DSA的具体实现，以及测试工具、性能测试工具、构建目标和专属的形式化验证文件夹。

苹果表示，形式化验证文件夹中包含了用于验证其实现是否符合FIPS 203与FIPS 204标准的证明材料及配套工具。上述两项标准分别对应NIST发布的ML-KEM（用于建立安全加密密钥）和ML-DSA（用于数字签名）规范，旨在抵御未来量子计算机所带来的已知安全威胁。

除代码仓库外，苹果还同步发布了一篇详尽说明，介绍在对外公开代码之前如何对其进行验证，以及此次发布的目的与意义。

苹果在公告中表示："随着2026年5月22日corecrypto源代码的最新发布，我们将在应用形式化验证领域取得的重要进展与全球密码学社区共享，包括我们的方法论细节和所使用的工具。此次公开发布旨在推动更广泛的采用，支持外界对我们工作的独立审查，并助力提升关键软件安全保障领域的整体水平。"

整个验证流程极为复杂，综合运用了常规测试、仿真、独立审查以及苹果自主研发的形式化验证方法。

苹果表示之所以开发定制化方案，是因为现有工具无法满足其全部需求——corecrypto需要在苹果全线产品上运行，涵盖搭载不同苹果芯片设计的设备。此外，苹果的实现方案同时包含可移植的C语言代码和针对自研处理器手工优化的ARM64汇编代码，仅靠现有验证方法远远不够。

苹果表示，此项工作有效发现了常规测试在代码进入产品之前无法察觉的问题。

苹果举例说明："我们在早期的ML-DSA实现中发现了一个缺失步骤，在极少数情况下可能导致输入数据超出预期范围并产生错误输出。我们还发现了第三方证明中的一处错误，并针对我们实现所使用的具体参数值进行了独立修复。在最坏的情况下，该缺失步骤可能在现有测试套件毫无警示的情况下，悄无声息地破坏密码学计算结果。将形式化验证融入开发周期，为我们的实现正确性以及各子程序协同工作的可靠性提供了有力保障。"

此外，苹果还向安全研究人员提供了以下参考资料：《苹果corecrypto形式化验证》研究论文（详细阐述了其验证方法）、定制开发的Cryptol-to-Isabelle转译工具（用于将苹果部分验证工作转换为可与官方标准进行核对的格式），以及corecrypto源代码归档中的Isabelle理论文件（为专家提供了用于复现和评估苹果验证结果所需的底层证明材料）。

Q&A

Q1：苹果发布的corecrypto是什么？有什么用途？

A：corecrypto是苹果底层密码学库，被苹果安全框架、CryptoKit和CommonCrypto所使用，负责支撑加密、哈希、随机数生成和数字签名等核心功能。此次苹果将其源代码公开发布在GitHub上，供全球安全研究人员审查与参考，也是苹果推进后量子密码学工作的重要组成部分。

Q2：苹果的PQ3协议是什么？能解决什么问题？

A：PQ3是苹果随iOS 17.4发布的后量子加密协议，用于为iMessage提供后量子级别的安全保护。它在会话启动时以及加密密钥定期刷新时均能抵御未来量子计算机的潜在攻击，是苹果在后量子密码学领域迈出的第一个重要公开步骤。

Q3：苹果为什么要自己开发形式化验证工具？

A：因为现有工具无法完全满足苹果的需求。corecrypto需要在搭载不同苹果芯片的全线设备上运行，实现方案同时包含可移植C语言代码和手工优化的ARM64汇编代码，现有验证方法难以覆盖所有场景。苹果因此开发了定制化验证方案，并通过此方法发现了早期ML-DSA实现中普通测试无法察觉的缺陷。