Apple corecrypto 形式化验证蓝图

# Apple corecrypto 形式化验证蓝图 - Apple 安全研究 来源：https://security.apple.com/blog/formal-verification-corecrypto 作者：Apple 安全工程与架构 (SEAR) 及硬件技术形式化验证团队 iMessage 中引入量子安全加密算法（https://security.apple.com/blog/imessage-pq3/）标志着一次重大安全转型的开始，旨在保护 Apple 用户免受未来量子计算机构成的威胁。为了在所有 Apple 平台上大规模部署这一代新算法，需要高置信度保障，因此我们开发了严格的新形式化验证方法，以证明我们实现的数学正确性。随着本周 corecrypto 的发布，我们将量子安全 ML-KEM 和 ML-DSA 算法的实现 — 以及我们为证明它们忠实于 FIPS 203 和 FIPS 204 规范而构建的数学证明 — 公之于众，供专家独立评估。此外，为了进一步推动关键软件保障技术的进步，我们还发布了为达到这些相关算法任何广泛部署的生产实现中已知最强正确性结果而创建的形式化验证库和工具。 --- 形式化验证过程（图片） 2024 年，我们在 corecrypto（Apple 操作系统中的基础加密库）中增加了后量子加密功能。为了应对未来量子计算机带来的已知威胁，我们一直致力于首先在最可能受益的领域开发和部署强大的量子安全加密：涉及加密通信和其他敏感信息的应用，包括 iMessage、VPN 和 TLS 网络（https://support.apple.com/guide/security/quantum-secure-cryptography-apple-devices-secc7c82e533/1/web）。此外，去年秋季发布的 Apple CryptoKit（https://developer.apple.com/documentation/cryptokit/enhancing-your-app-s-privacy-and-security-with-quantum-secure-workflows）中附带的量子安全 API 使开发者能够在其自身应用中采用量子安全加密和认证。 corecrypto 在我们的产品中持续使用，为超过 25 亿台活跃设备提供加密解密、哈希、随机数生成和数字签名功能。corecrypto 中的关键错误有可能危及依赖它的每个应用和功能的安全性和可靠性，因此我们在向该库添加新代码时持保守态度，并付出非凡努力进行全面测试。 只有在根据以下标准进行全面评估后，我们才会将新的加密算法纳入 corecrypto： 1. **提升安全性**。算法必须解决新问题或改进现有算法的安全性。 2. **安全设计**。算法必须具有强大的理论安全性，并且必须经受住了全球研究界严格、持续的密码分析。实际上，必须能够以安全的方式为我们预期的用途实现该算法。 3. **高性能**。在所有 Apple 设备上实现时，执行必须高度高效 — 无论是在延迟还是功耗方面。 4. **紧凑参数**。密钥大小、签名和密文必须最小化对网络延迟的影响，并适合设备内存限制。 当某算法满足我们纳入 corecrypto 的高标准时，我们开发的实现必须随后满足： 1. **安全性**。代码必须满足严格的安全标准，且不得泄露信息。这既需要正确性也需要强化，例如防止泄露攻击者可用于提取应用秘密的时序信号。 2. **优化**。实现应最大程度利用其所运行芯片的指令和架构。 3. **正确性**。代码（包括所有相关优化）必须忠实地实现密码学界已分析的标准中定义的算法。它必须产生正确的输出。 当我们评估要纳入 corecrypto 的量子安全算法时，我们迅速聚焦于两个符合我们标准的算法 — 也就是后来被 NIST 选择并标准化为 ML-KEM 和 ML-DSA（分别为 FIPS 203 和 FIPS 204）的相同算法。虽然 NIST 还标准化了其他签名方案，但 ML-KEM 和 ML-DSA 最符合我们的需求。密码学界的重大工作已经为 ML-KEM 和 ML-DSA 产生了参考实现，在我们自己的评估中，这些实现显示出安全性和性能的坚实基础。 由于 corecrypto 用于 Apple 产品（包括具有不同微架构的专用芯片），我们首先用可移植的 C 代码编写算法实现。为了确保实现能在部署 corecrypto 的任何地方正确安全地运行，我们的指导方针很严格：我们编写此代码以避免通过执行时序泄露秘密值，防止编译器无意中削弱这些保护，并利用 Apple 处理器上的硬件特性，如数据独立时序 (DIT) 和指针认证 (PAC)，它们分别防御一系列微架构侧信道攻击并强化内存损坏攻击的防御。此外，我们根据特定用途的威胁模型评估对内部计算进行随机化的需求。 在审查了 ML-KEM 和 ML-DSA 设计附带的参考实现后，我们发现了进一步改进的重要机会。我们应用了数学优化，在不改变底层算法的情况下提高性能，并仔细重写了最影响性能和安全性的子例程，以充分利用我们业界领先的处理器。凭借我们在 Apple 芯片方面的深厚专业知识，这些手工优化的路径还使我们能够精确控制处理器行为，从而帮助防止可能向攻击者暴露秘密的时序侧信道。 引入这些包含我们重大改进的复杂算法的新颖实现是一项重大工程。使挑战更大的是，ML-KEM 和 ML-DSA 所基于的数学本身相对较新，因此业界在安全地将这些算法部署到成品中的集体经验要少得多。在每一步，我们都深受驱动，以避免业界早期部署椭圆曲线加密时遇到的问题，当时这些问题因微妙且可利用的错误而受阻。 我们的首要任务是确保新的算法实现（包含我们为性能和安全强化而手工调整的优化）在功能上正确且安全。为了实现这一目标，我们设定了一个特殊的资格门槛，包括深入的常规测试、模拟和独立审查，并将其与严格的形式化验证相结合。 ### 我们的形式化验证要求 形式化验证使用数学证明来证明系统或对象满足我们定义的特定属性。在 Apple，我们在芯片开发中进行了超过 15 年的广泛形式化验证，并在 2019 年开始使用形式化验证来证明经典密码学，包括硬件公钥加速器 (PKA) — 执行椭圆曲线公钥运算的 Apple 芯片部分。 对于 corecrypto，我们使用数学证明来表明我们的算法实现比常规软件测试允许的保证程度显著更高。简而言之：如果我们能证明我们实现的数学公式与其规范等价，那么我们就知道我们的实现将产生正确的输出。理论上，这给了我们很强的保证，即我们的实现每次都能正确工作。这种高度的保证通常无法通过常规测试获得。 实际考虑更为复杂。无论以何种方式应用，形式化验证都需要巨大的时间投入和深厚的专业知识。实现及其规范必须用精心选择的数学公式来表示。为了得出正确的结论，公式必须正确地建模实现和规范的相关行为，并且其结构必须能够使证明以简单步骤编写。公式还必须足够完整，以涵盖我们需要的所有输入。由于生成的公式可能非常巨大，需要专业的工程技能 — 包括对底层数学的深刻理解 — 才能编写数学证明，并掌握用于逐步验证这些证明的工具。成功构建验证的证明策略通常需要多次迭代。 通过分析如何最好地将 ML-KEM 和 ML-DSA 的形式化验证与我们现有的工程流程相结合，我们为 corecrypto 的形式化验证制定了关键要求。 在实践中，我们选择的算法具有多个功能：ML-KEM 中的密钥生成、封装和解封装，以及 ML-DSA 中的密钥生成、签名生成和签名验证。这些功能中的每一个都由一系列专门的子例程实现，这些子例程传统上容易出现微妙的算术错误，特别是对于多项式和大数等大操作数。这些子例程通常涉及计算过程中的进位或借位，实现需要正确处理，但由于数量过多且在子例程序列中太深，无法通过常规测试彻底检查。 形式化验证有助于证明这些子例程中的每一个都能在指定输入上产生正确的输出。但单独验证每个子例程是不够的，因为优化的子例程可能以略微不同的方式表示对象，并且如果未证明一个子例程的输出与序列中的下一个子例程完全兼容（例如，当中间子例程的输出值落在下一个子例程支持的输入范围之外时），可能会遗漏错误。 这些细节帮助塑造了我们对 Apple corecrypto 形式化验证的关键要求： - 我们的形式化验证必须**能够验证我们的整个算法实现**，包括我们高级的数学公式。它必须能够证明每个子例程单独产生正确的输出，并且完整的子例程序列共同计算出正确的最终结果。 - 为了考虑到使用 corecrypto 的多种产品，我们的验证必须**支持用可移植 C 语言和 ARM64 汇编语言（Apple 芯片使用的指令语言）编写的算法实现**。 - 由于我们不断改进软件以优化实现并支持新的应用，我们的验证必须支持**快速演进**，并最小化保持正确性证明有效所需的工作量，包括保持与我们现有开发者工具的兼容性。 ### 针对 corecrypto 的自定义方法 为了找到正确的方法，我们评估了许多验证工具和现有的已验证实现。大多数不符合我们的要求。一些工具缺乏对 ARM64 的支持，其他工具只验证混合语言实现的一部分 — 一次一种语言 — 而不评估我们使用的子例程或子例程序列的正确性，或者它们会要求我们在所有使用 corecrypto 的地方构建和维护广泛的新的开发者工具。 为了满足我们独特的要求 — 包括支持多种语言、快速代码演进和现有开发者工具 — 我们最终为形式化验证设计了一种自定义方法。我们结合了已经使用的工具和我们能够满足全部要求并追求自底向上证明的新工具，这些证明从我们的最终实现一直回溯到 ML-KEM 和 ML-DSA 的 FIPS 规范。 高级形式化验证过程在本页顶部的图片中描绘。通过将规范 — NIST 标准化的 ML-KEM 和 ML-DSA — 以及我们的实现翻译成形式化数学，我们可以通过组合关于我们优化的 C 和 ARM64 实现的增量证明来展示功能正确性。 --- *在这篇文章中，我们主要引用以下用于形式化验证的开源工具：* - ***Isabelle**：一种形式化语言和强大的证明助手，可以验证复杂的数学证明。我们已使用 Isabelle 来验证硬件 PKA。* - ***软件分析工作台 (SAW)**：由 Galois 开发的工具，用于根据用领域特定语言 Cryptol 编写的规范来形式化验证软件程序的属性。* - ***Cryptol**：一种与 SAW 配合使用的形式化语言，也由 Galois 开发。* - ***cryptol-to-isabelle**：Galois 根据我们的规范创建的新工具，用于将我们的 Cryptol 算法模型翻译成 Isabelle 公式，以便与我们的算法的 Isabelle 规范进行比较。* --- 首先，我们将每个算法的可移植 C 实现手动翻译成 Cryptol 语言。然后，我们使用 Cryptol 的配套工具 SAW 来验证我们的 Cryptol 模型与我们的实现匹配。我们选择 Cryptol 是因为 SAW 非常擅长推理 C 语言，但它缺乏对 FIPS 规范中高级数学的支持，因此我们需要为后续步骤寻找共同基础。 为了证明我们的 Cryptol 模型与规范等价，我们需要一个表达力足够强且足够强大的环境，以便我们能够证明这些非常不同的表示之间的等价性。由于 Isabelle 已经满足这个标准，我们使用一个专用的翻译器 — 由 Apple 指定并由 Galois 构建 — 直接从 Cryptol 在 Isabelle 中生成一个实现模型。这也有助于消除两种语言之间桥接时人为错误的风险。我们还细致地手动将 FIPS 规范翻译成 Isabelle。 现在模型和规范都已翻译成 Isabelle，我们可以编写证明来展示它们在完整算法（包括其子例程）上的等价性。然而，鉴于涉及大量不同且复杂的子例程，所需工作量相当大，需要超过 50,000 个证明步骤。为了更好地扩展这种方法，我们将大量精力用于构建一套新的 Isabelle 库 — 可重用的理论，主要是可应用于跨子例程证明的引理，使它们更简洁、编写更快。一旦整个证明能够在 Isabelle 中运行并通过验证，我们就证明了我们的 C 实现与算法规范的等价性。 我们方法的最后一步是验证用 ARM64 汇编编写的手工优化子例程。CPU 指令序列在概念上与其数学规范相距甚远，这使得直接等价证明复杂得多。然而，将汇编指令与相应的 C 实现进行比较时，挑战就更容易处理。这正是我们采用的策略：随着两个实现模型都被翻译成 Isabelle，我们证明每个 ARM64 子例程与它所替换的 C 子例程等价。并且由于 C 实现中的每个 C 子例程都已被证明并验证为正确，这为我们提供了对优化子例程正确性的强有力保证。