苹果今天在 GitHub 上发布了新的 corecrypto 源代码，同时还附上了一篇详细的技术文章，解释他们在 iPhone、Mac 等设备上推进后量子加密工作的具体细节。
苹果持续推进后量子安全工作
今天早些时候，苹果在 GitHub 上新建了一个 corecrypto 代码仓库，这是他们后量子加密工作的又一次重要更新。这项工作从 2024 年 iMessage 的 PQ3 协议开始，就已经逐步向公众开放。
PQ3 是随 iOS 17.4 一起发布的，它是苹果在对抗未来量子计算机威胁方面迈出的第一大步。iMessage 不仅在对话开始时提供后量子保护，还会在加密密钥定期刷新时持续加强安全。
今天的发布延续了这项努力。GitHub 仓库里包含了 corecrypto 的源代码，这是苹果 Security 框架、CryptoKit 和 CommonCrypto 底层使用的加密库，负责加密、哈希、随机数生成和数字签名等功能。
仓库中还包括苹果自己实现的 ML-KEM 和 ML-DSA（他们为 corecrypto 选定的两种后量子算法），以及测试代码、性能工具、构建配置，还有一个专门的正式验证文件夹。
苹果表示，这个正式验证文件夹里存放了证明材料和相关工具，用来确保他们的实现符合 NIST 的 FIPS 203 和 FIPS 204 标准。其中 ML-KEM 用于建立安全的加密密钥，ML-DSA 用于数字签名，目的是抵御未来量子计算机已知的攻击威胁。
苹果详细介绍后量子安全工作
除了代码仓库，苹果还发布了一篇非常详尽的文章，说明他们在把代码公开给外部审查之前是如何验证的，以及为什么选择现在发布这些内容。
随着 2026 年 5 月 22 日 corecrypto 源代码的最新发布，我们向全球加密社区分享了应用形式验证方面的重大进展，包括我们的方法细节和所使用的工具。这些内容全部公开，就是为了鼓励更广泛的采用、支持对我们工作的严格审查，并推动保障关键软件的技术进步。
整个验证过程非常复杂，结合了常规测试、模拟运行、独立审查以及苹果自家的形式验证工作。
苹果说，他们之所以要开发一套自定义的方法，是因为现有的工具无法完全满足需求——corecrypto 需要在苹果全线产品上运行，包括不同 Apple 芯片设计的设备。而且他们的实现既有可移植的 C 代码，也有针对自家处理器的 ARM64 汇编优化代码。所以只靠现有验证方法是不够的。
正如苹果所解释的，这项工作帮助他们在代码进入产品之前发现了常规测试难以察觉的问题。
举例来说，我们在早期 ML-DSA 实现中发现了一个缺失的步骤，在极少数情况下可能导致输入超出预期范围并产生错误输出。我们还发现了一个第三方证明中的错误，并针对我们实现所用的具体参数值独立进行了修复。最坏的情况下，这个缺失步骤的问题可能会在没有任何现有测试套件警告的情况下悄无声息地破坏加密计算。将形式验证融入开发流程，为我们的实现正确性以及每个子程序之间的协同工作提供了强有力的保障。
最后，苹果还推荐了他们的技术论文《Formal verification for Apple corecrypto》（详细阐述了验证方法）、自研的 Cryptol-to-Isabelle 转换工具（帮助把部分验证工作转换为可对照官方标准的格式），以及 corecrypto 源代码归档中的 Isabelle 理论文件（为安全研究人员提供了重现和评估苹果结果所需的底层证明材料）。
你可以在这里阅读苹果安全研究博客的完整文章，也可以在此处查看 GitHub 仓库。
