守护未来：Apple 对 corecrypto 进行形式化验证的蓝图
向量子安全密码学的过渡不再仅仅是一项理论练习；它已成为生产环境的必然要求。随着将后量子加密集成到 iMessage 和其他关键服务中，Apple 面临着一项艰巨的任务：在超过 25 亿台活跃设备上部署新算法——ML-KEM 和 ML-DSA。
鉴于 corecrypto 中的单个关键漏洞可能会危及依赖它的每个应用和功能的安全性，Apple 已超越了传统的测试方法。他们实施了一套严谨的形式化验证蓝图，以证明其实现的数学正确性，确保其忠实于 FIPS 203 和 FIPS 204 规范。
corecrypto 的高标准
向 corecrypto 添加新算法是一个非常谨慎的过程。Apple 根据四个主要标准评估候选算法：提高安全性、经过全球密码分析验证的安全设计、高性能（延迟和功耗）以及紧凑的参数以最大限度地减少网络影响。
一旦算法被选中，其实现必须满足三个严格的要求：
- 安全性：代码必须防止信息泄漏，特别是要防范时序侧信道攻击。
- 优化：实现必须最大限度地提高底层 Apple silicon 的效率。
- 正确性：代码必须忠实地实现标准，并始终产生正确的输出。
形式化验证的挑战
虽然传统测试至关重要，但它无法提供与形式化验证同等水平的保证。形式化验证使用数学证明来演示一个系统满足特定属性。然而，这个过程是资源密集型的，需要深厚的数学专业知识，以及对实现和规范进行精确建模。
对于 corecrypto，Apple 识别出了在用于密钥生成、封装和签名的专门子程序序列中的特定风险。这些子程序通常涉及具有大操作数（多项式和大数）的复杂算术运算，其中进位或借位可能会导致微妙的漏洞。
验证孤立的子程序是不够的；验证必须证明一个子程序的输出与下一个子程序的输入范围完全兼容。
定制化验证流水线
由于现有工具通常缺乏对 ARM64 assembly 的支持，或者需要放弃现有的开发工具，Apple 设计了一种结合了多种专门工具的定制化方法：
工具链
- Cryptol：一种用于创建算法模型的形式化语言。
- Software Analysis Workbench (SAW)：用于验证 Cryptol 模型是否与 C 实现匹配。
- Isabelle：一种强大的证明助手，用于验证复杂的数学证明。
- cryptol-to-isabelle：由 Galois 构建的定制翻译器，用于弥补 Cryptol 模型与 Isabelle 公式之间的差距。
流程流
- C 转 Cryptol：可移植的 C 实现被手动翻译成 Cryptol。然后 SAW 验证 C 代码是否与该 Cryptol 模型匹配。
- Cryptol 转 Isabelle：Cryptol 模型被翻译成 Isabelle。同时，FIPS 规范也被手动翻译成 Isabelle。
- 等价性证明：使用 Isabelle，工程师编写了证明（超过 50,000 步）来展示实现模型与规范是等价的。 为了扩展这一规模，Apple 开发了一个包含可重用 Isabelle 理论和引理的库。
- Assembly 验证：为了处理经过手工优化的 ARM64 assembly，Apple 证明了每个 assembly 子程序与相应的已验证 C 子程序是等价的。 这避免了从头开始针对高层规范验证 assembly 的需求。
现实世界的影响与结果
这一严谨的过程带来了切实的安全性提升。Apple 发现了一个早期 ML-DSA 实现中的缺失步骤，该步骤可能导致输入超出预期范围，从而可能在不经意间损坏密码学计算。
他们还发现并修复了一个第三方证明中的错误。
正如社区所指出的，这些正是传统测试难以发现的漏洞类型：
"ML-DSA 早期实现中的缺失步骤漏洞是 SAW 的完美案例。那些罕见的输入可能会通过代码审查，因为本该在那里的那一行看起来并不像是缺失的，它看起来像是下一行是正确的。"
局限性与补充方法
形式化验证并非万能灵药。Apple 承认存在特定的局限性：
- 编译器信任：该方法假设编译器能从已验证的 C 代码正确地生成 CPU 指令。
- 工具链差距：SAW 的某些局限性意味着 ML-DSA 的所有可能消息大小都无法被验证，因此在这些特定情况下需要回退到传统测试。
为了弥补这些差距，Apple 将形式化验证与仿真工具以及广泛的传统测试相结合，以保护用户免受信息泄漏和其他非功能性漏洞的影响。
通过开源其 Isabelle 理论和 Cryptol-to-Isabelle 翻译器，Apple 旨在鼓励这些 wider adoption 这些方法，推动行业向一个标准迈进：即关键密码学软件是通过设计来证明其正确性的，而非仅仅通过测试来获得稳定性。