5月22日，苹果安全工程与架构团队（SEAR）和硬件技术形式化验证团队正式发布CoreCrypto 后量子密码学形式化验证框架，并就包含ML‑KEM、ML‑DSA算法实现与完整数学证明的corecrypto最新源码进行开源。
这些成果的发布与开源，主要目的是想向全球密码学界开放且鼓励广泛应用，同时对苹果工作进行批判性审查，加速关键软件安全保障技术发展。
基于此，我们今天不聊量子领域老生常谈的话题，我们来聊聊苹果这套形式化验证框架，对于后量子密码学（PQC）的发展甚至于商业化落地究竟有多大助力。
为什么需要形式化验证？
2024年，苹果把后量子加密技术加入到其Apple操作系统基础加密库corecrypto中，为超过25亿台活跃设备提供加密、解密、哈希、随机数生成、数字签名等基础能力。
corecrypto里的一个严重缺陷可能会损害所有应用和功能的安全与可靠性，甚至可能会带来灾难性的后果。因此，苹果在加入新的代码到库中时是慎之又慎。
苹果在多个选择中评估出了2种符合苹果要求的方案，即NIST标准的ML-KEM（FIPS 203，密钥封装过程）和ML-DSA（FIPS 204，数字签名），这些算法都基于格的密码学。
传统的软件测试就像是随机抽样检验。测试的人采用一些测试数据输入后，看看输出结果对不对就可以了。这种方法面对小概率出现的问题，糟糕的触发点一下子就原形毕露。
形式化验证就不一样。它是将代码和算法规范都转化为数学公式，然后用一系列证明式推导验证两者完全相等即可。也就是形式化验证并不是“运行”代码，而是在“推导”代码运行的正确性。
苹果公司官方博客表示，后量子密码学（PQC）算法ML-KEM和ML-DSA目前的情况是比较尴尬的，因为两者的数学原理有些新奇，整个业界还没有足够的经验把这些概念部署到实际产品中。
苹果有一个很好的例子，它发生在十分具体的设计上：在早期的设计中，形式化验证工具发现了一段ML-DSA的实现里缺少了一个重要的步骤。通常的情形下，错误的输入值超出这种情形的预期范围，会悄悄破坏加密计算，而常规测试套件通常会忽视这种情况。
这类错误，靠人工审查代码几乎无法定位。这就是形式化验证的价值。它证明了苹果的C语言实现、ARM64汇编优化的实现与NIST发布的FIPS 203、FIPS 204的数学完整性完全等价。
形式化验证
形式化验证就是不跑代码，将代码里的逻辑全部文字化成公式的数学世界，然后逻辑推算形式化证明这些代码实现了NIST公布的数学规范，且在任何无限可能的输入下都是绝对等价的。
但搞形式化验证极为烧钱且费人。苹果公司已经在芯片上进行了超过15年的普遍形式化验证，并于2019年开始使用形式化证明经典密码，包括设备级硬件公钥加速器(PKA)。
但这次要在软件的C语言，甚至是底层的ARM64汇编上大动干戈，于是，苹果将早已使用的工具和新工具结合起来，发明了一种定制的形式化验证方法。
Isabelle：一种形式化语言和强大的证明辅助工具，可以验证复杂的数学证明。苹果已经使用Isabelle来验证硬件PKA。
软件分析工作台（SAW）：由Galois开发的工具，用于根据用名为Cryptol的领域特定语言编写的规范，对软件程序的属性进行形式化验证。
Cryptol：一种与SAW配合使用的形式化语言，同样由Galois开发。
cryptol-to-isabelle：Galois根据苹果的规范创建的新工具，用于将Cryptol算法模型转换为Isabell公式，以便将其与苹果算法的Isabelle规范进行比较。
来源：苹果
而且，苹果并没有推翻之前的东西。他们针对最底层的ARM64汇编优化代码，采取了一种“等价性”证明：
由于C语言版本已被证明和验证正确，那么他们只要证明保证优化后的ARM64汇编实现的正确性，这样就可以了，完全没必要花费大量的时间和精力从头逐一验证形式化规范。
上述的验证方法，能够为任何广泛部署的ML-KEM和ML-DSA生产实现提供目前最高的函数正确性保证，并且它完全支持手工优化代码。
为什么对量子安全行业至关重要？
苹果这次推出的后量子密码学形式化验证工具框架对量子安全行业为什么很重要呢？根本原因就是一个词，时间。量子安全迁移，最重要的就是时间。
早的在2024年8月，NIST已敲定了FIPS 203、FIPS 204等相关标准，美国CISA和NSA等已经有了2033年的硬性“迁移”时间表。理论上，所有的企业和开发人员都应该努力把RSA和ECC算法换成后量子算法。
为什么现实不是这样？
大家都知道，密码学是一个非常敏感的领域，历史上经验告诉我们，哪怕最小的实现差错都会导致整体的溃败。至于椭圆曲线密码学(ECC)初用中出现的隐蔽性弱点就是最好的例子。
苹果这次开源除了给大家分享代码以外，还传递了一种“安全感”。开源这么一套形式化验证框架，苹果就是把自己的尺子送给了开发者。
尤其是对于那些需要跑在ARM Cortex-M0+这类极其受限的物联网设备上的PQC实现，苹果证明了高安全性和高能效完全可以同时实现。
用苹果的话来说，核心库corecrypto支撑着全球超过25亿台活跃设备。全球如此之大的体量系统都能用形式化验证来保证“零误差”，金融、医疗、军工等领域的量子安全升级就有了可参照的范本。
对于国内的科技企业和密码学学术机构来讲，这也是个警钟。其在推动国家相关抗量子标准落地时，也要在工程落地的质量检验方面把好关。
从“被动跑库”到“主动数学求证”转型，同时在自研硬件架构上完成形式化验证的闭环，已成为我们必须啃下的硬骨头。
毕竟，在这个绝对理性的密码学世界里，从来没有侥幸二字。
[1]https://security.apple.com/blog/formal-verification-corecrypto/
[2]https://dig.watch/updates/apple-quantum-secure-cryptography
