苹果开源 corecrypto：用数学证明保证量子安全

5 月 22 日，苹果在 Apple Security Research 博客上宣布开源 corecrypto 源代码，公开了 ML-KEM 和 ML-DSA 两种量子安全密码算法的实现，并首次附带端到端的形式化验证数学证明。这些证明确保了 C 代码和手工优化的 ARM64 汇编实现与 NIST 标准规范严格一致。

corecrypto 是 Apple 操作系统的底层密码库，为 iMessage、VPN、TLS 等加密通信场景提供运算支持，覆盖超过 25 亿台活跃设备。2024 年苹果已将后量子加密集成到 iMessage 中，去年秋季发布的 Apple CryptoKit 也开放了量子安全 API 供开发者使用。

什么是形式化验证

传统软件测试的方法本质上是抽样检查：构造一组输入，运行程序，观察输出是否符合预期。但密码学实现面对的是任意可能的输入空间，测试用例再密集也只能覆盖极小的一部分。某些微妙的算术错误——例如多项式运算中的进位处理遗漏——可能长期潜伏在生产环境中而不被常规测试捕获。

形式化验证的思路完全不同：它使用数学证明来论证"对于所有合法输入，程序的行为与规范严格一致"。如果传统测试是"开车跑了一圈没撞墙"，形式化验证则是"用数学证明这台车在任何条件下都不可能撞墙"。

代价是极高的工程复杂度。实现代码和规范必须被转化为精确的数学公式，这些公式必须正确建模两者的行为、覆盖所有输入、并允许证明以可管理的步骤推进。苹果在芯片验证领域积累超过 15 年经验，2019 年开始将形式化验证扩展到经典密码学硬件（PKA 公钥加速器），这次是首次将该方法论完整应用到软件层面的量子安全算法。

四层证明链：从规范到汇编

苹果设计的验证方法形成了一条从 NIST 标准到最终机器指令的完整证明链：

第一层：NIST 规范 → Isabelle 形式化。 苹果将 FIPS 203（ML-KEM）和 FIPS 204（ML-DSA）标准规范手工翻译为 Isabelle 证明助手中的数学公式。

第二层：C 实现 → Cryptol 模型。 将可移植 C 代码实现翻译为 Galois 开发的 Cryptol 语言（一种面向密码学的形式规约语言），再通过 SAW（Software Analysis Workbench）工具验证 Cryptol 模型与 C 实现等价。

第三层：Cryptol → Isabelle 对比证明。 利用苹果定制、Galois 开发的 cryptol-to-isabelle 翻译器，将 Cryptol 模型自动转为 Isabelle 公式，然后证明它与第一层的 NIST 规范形式化等价。这一步需要超过 50,000 个证明步骤，苹果为此构建了可复用的 Isabelle 理论库（库、引理、分离代数框架）来提高证明效率。

第四层：ARM64 汇编 → C 实现等价证明。 手工优化的汇编代码在数学上距离规范太远，直接与规范做等价证明代价极高。苹果的策略是：在 Isabelle 中证明每条 ARM64 子程序与其对应的 C 子程序等价。由于 C 子程序已经通过前三层证明了正确性，汇编的正确性也得到传递保证。

验证发现了什么

形式化验证的实际价值在这次项目中得到了具体体现。苹果在验证过程中发现了两类问题：

第一类是 ML-DSA 实现中的一个遗漏步骤。在特定边界条件下，输入值可能超出预期范围并产生错误输出。这个问题在常规测试中无法触发——测试用例的设计几乎不可能覆盖到这个路径，但数学证明系统地遍历了所有输入空间。在最坏情况下，这个缺陷会导致密码学计算被静默篡改，而现有测试套件不会给出任何警告。

第二类是第三方证明中的一个错误，苹果独立修复了与具体参数值相关的证明缺陷。

为什么需要定制方法

苹果评估了现有的形式化验证工具和已验证的实现，发现没有一个能满足 corecrypto 的全部需求：部分工具不支持 ARM64 指令集；部分工具只支持单语言验证（C 或汇编二选一），无法证明跨语言子程序序列的联合正确性；部分方案需要搭建和维护庞大的开发者工具链，与苹果现有工程流程不兼容。

最终苹果采用了定制的混合方案：Isabelle 负责高级数学推理和规范对比，SAW/Cryptol 负责 C 代码验证，cryptol-to-isabelle 作为两个世界的桥梁，ARM64 模型在 Isabelle 内与 C 实现做等价证明。这种分层设计允许单独替换某个子程序而无需重写整条证明链，支持快速迭代。

局限性与公开内容

苹果也坦诚了方法论的局限：证明假设编译器行为正确（即编译器不会引入错误）；SAW 工具的局限导致 ML-DSA 的部分消息长度未被完全覆盖，苹果通过常规测试和核心置换子程序的验证来弥补这一缺口。

此次开源的内容包括：corecrypto 源代码、形式化验证技术论文、cryptol-to-isabelle 翻译器、Isabelle 理论库（ARM64 模型、精化框架、SProp 分离代数库、FIPS 形式化定义）。部分理论库以宽松许可证发布，允许社区直接使用和扩展。

苹果在 corecrypto 上投入形式化验证的动机很清晰：一个为 25 亿设备提供加密服务的基础设施，任何未捕获的缺陷都可能产生系统性影响。椭圆曲线密码学的早期部署曾因隐蔽的算术 bug 导致安全问题，苹果明确希望避免重蹈覆辙。对于更广泛的工程社区，corecrypto 的形式化验证提供了一个可参考的生产级范例，公开的工具链和理论库降低了后续项目的进入门槛。

来源：Apple Security Research