后量子密码学的高性能验证与优化

验证并优化某机构的后量子密码学

自动化推理如何协调安全性、性能和可维护性之间的需求。

作者：Hanno Becker, Rod Chapman, Dusan Kostic

2026年4月7日

13分钟阅读

摘要

Mlkem-native 是一个高 assurance、高性能的 ML-KEM C 语言实现，它将参考实现的简洁性与研究优化和形式化验证相结合。使用 CBMC 和 SLOTHY 等自动化工具来确保内存安全、类型安全和功能正确性，从而能够以数学确定性进行激进的汇编优化。与 ML-KEM 参考实现相比，Mlkem-native 在不同 EC2 实例上实现了显著的性能提升，每秒操作数增加了 2.0 到 2.4 倍，同时保持了安全性和可维护性。

如今，安全的在线通信由公钥密码学实现，主要是 RSA 和椭圆曲线密码学（ECC），其安全性依赖于某些计算问题难以处理的假设。然而，虽然传统计算机认为这些问题难以处理，但 RSA 和 ECC 所依赖的问题对于足够大的量子计算机来说可能是可处理的。“先存储，后解密”攻击——即拦截加密信息并保存，直到量子计算机能够解密——需要在攻击技术可行之前就对其进行防护。后量子密码学（PQC）是在经典计算机上运行但面对量子计算仍安全的密码学。2024 年，经过八年的标准化工作，美国国家标准与技术研究院（NIST）发布了标准 FIPS-203，该标准将模块格基密钥封装机制（ML-KEM）指定为一种密钥协商机制，被认为能够抵御量子计算机的攻击。

在这篇文章中，我们描述了某机构的自动化推理团队、某机构密码学团队和开源社区如何合作创建了一个开源、经过形式化验证且优化的 ML-KEM 实现，以最高 assurance 和最低成本保护客户免受“先存储后解密”攻击。

什么是良好的密码工程？

秉承某机构以客户为中心的宗旨，我们在处理密码解决方案时优先考虑三个目标：

• 客户数据的安全性：密码学以难以安全实现而闻名，任何缺陷都可能危及客户隐私；
• 客户体验：密码学是一种计算开销，我们将其最小化，以确保为客户提供最低的成本和最佳体验；
• 我们维护解决方案的能力：花在维护上的时间越少，我们就能有越多时间为客户进行创新。

然而，这些目标之间存在矛盾：简单的代码最容易维护和安全编写，但往往运行缓慢。快速的代码往往更难审计且容易出错。

自动化推理使我们能够解决这些矛盾，并为客户提供安全、快速且可维护的密码解决方案。

又一个 ML-KEM 实现？

ML-KEM——以前称为 Kyber——从实现角度来看已被充分研究：一方面，Kyber 参考代码提供了一个简洁的 C 实现，多年来一直受到 scrutiny。另一方面，大量研究论文描述了如何针对不同指标和平台优化 ML-KEM。

2024 年，某机构密码学团队和某机构自动化推理团队面临的挑战是，将参考实现的简洁性与研究工作中揭示的优化潜力结合到一个可用于生产的实现中：mlkem-native。

大约在同一时间，某机构成为 Linux 基金会后量子密码学联盟（PQCA）的创始成员，该联盟创建了后量子密码学包（PQCP），“一个开源项目集合，旨在构建标准跟踪后量子密码算法的高 assurance 软件实现”。因此，我们的团队成员没有自己开发代码，而是加入了 PQCP，并很快推出了 mlkem-native，这是一个高 assurance、高性能的 ML-KEM C 语言实现，旨在将 ML-KEM 参考实现与优化和形式化验证的研究结合起来。

编码：慢与快

Mlkem-native 的模块化设计结合了一个覆盖 ML-KEM 高级逻辑的前端，以及一个负责所有性能关键子例程的后端。每个子例程——包括 SHA3 基础的 Keccak 置换和快速多项式算术基础的数字变换（NTT）——都有多个针对特定硬件本地编写的高效实现。除了默认的 C 实现外，mlkem-native 还为 AArch64、x86_64 和 RISC-V64 提供了汇编/内联后端。

对可维护性来说重要的是，前端和后端之间的接口是固定的：为新的目标架构添加优化的开发者根据后端规范实现选定的后端功能，而前端保持不变。后端规范的开发结果证明并不像听起来那么简单。

了解边界

内存安全性

C 编程语言的一个众所周知的挑战是缓冲区溢出的风险：写入超出内存区域指定限制可能会破坏数据结构，并且如果被恶意利用，可能导致非特权代码执行。此类问题的总称是内存安全。Rust 等内存安全语言可以限制越界访问的影响——例如，通过 panic 而不是表现出未定义行为——但它们并不能防止错误本身。

类型安全性

另一个众所周知的挑战（这次是关于实现 ML-KEM）是整数溢出的风险——这是类型安全的一个方面。与 RSA 和 ECC 一样，ML-KEM 依赖于模运算，其中操作结果除以特定数字——在 ML-KEM 的情况下，素数为 3,329，称为 MLKEM_Q 或简称为 q——并且只传递余数。取模运算符由百分号 % 表示。

从逻辑上讲，如果两个数字 x 和 y 需要在 ML-KEM 中相加或相乘，则需要计算 (x + y) % q 和 (x y) % q；例如，(294 38) % q = 11,172 % q = 1,185。这种“急切”的模 q 算术，不断应用模归约以在“规范”范围 {0, 1, 2, … , q-1} 中表示数据，速度慢得令人望而却步。

高效的 ML-KEM 实现使用“惰性”模 q 算术：尽可能长时间地对数据进行操作而不进行模归约，并且只有当存在溢出的最坏情况风险时才进行归约。此外，这允许使用不完美的归约算法，如 Montgomery 归约，这些算法很快，但并不总是给出完全归约的输出。

在 ML-KEM 的情况下，模 q = 3,329 的数据通常存储在 16 位有符号整数中。在处理 ML-KEM 中众多算术例程的惰性算术时，跟踪数据的最坏情况边界并在这些边界超过 16 位整数限制的地方插入模归约至关重要。这个领域的小错误可能会逃避测试——因为平均边界往往比最坏情况边界小得多——然后在生产环境中随机出现。

跟踪缓冲区边界，尤其是算术边界，既耗时又容易出错：例如，削弱低级算术函数的输出边界可能导致完全不同函数中罕见的算术溢出。手动检查这不仅需要细致的文档和熟练的审计员，还会减慢开发速度。

在 mlkem-native 中，我们使用一个名为 C 有界模型检查器（CBMC）的工具来自动验证 C 级别的内存安全性和类型安全性：对于每个函数，我们在源代码中添加机器可读和人类可读的契约，以指定缓冲区和算术数据的边界，并让 CBMC 自动验证，在这些边界内，不会发生缓冲区溢出或算术溢出。

案例：模归约

在代码示例中，__contract__ 部分定义了内存读写范围（内存安全）和返回值范围（类型安全）。mlk_barrett_reduce 函数建立对称输出区间，mlk_scalar_signed_to_unsigned_q 将其映射到目标区间。CBMC 自动验证这些规范是否按预期工作。

快速运行，保持安全

上述 CBMC 证明为 mlkem-native 的 C 代码建立了内存安全性和类型安全性。然而，mlkem-native 中性能最关键的部分——Keccak 置换和数论变换——是在 AArch64 和 x86_64 上用手工优化的汇编实现的。

为了在保持高性能的同时获得对 mlkem-native 中汇编实现的 assurance，我们使用了三个组件：SLOTHY（一个汇编超级优化器）、HOL Light（一个定理证明器）和 s2n-bignum（一个基于 HOL Light 构建的汇编验证基础设施）。它们共同实现了一个工作流，开发者编写清晰、可维护的汇编代码，而部署的代码则达到峰值性能并具有正确性的形式化保证。

手工编写高性能汇编产生了一个基本矛盾：清晰、可审计、明确表达计算的代码很慢，而快速的代码密集、特定于微架构且难以维护。SLOTHY 通过自动化特定于微架构的优化来解决这个矛盾：它将汇编程序转换为约束满足问题，使用约束求解器找到最佳指令调度和寄存器分配，并输出优化的汇编代码。开发者编写强调计算逻辑的清晰代码，SLOTHY 生成快速的代码。

我们使用 HOL Light 和 s2n-bignum 为所有 AArch64 和 x86_64 汇编例程证明功能正确性。在使用 SLOTHY 的地方，证明的编写方式与特定的指令顺序和寄存器分配无关；因此，我们可以针对特定微架构重新优化代码，而无需调整证明。这种“事后”验证方法确立了汇编所代表的计算的数学正确性，无论它是如何产生的；特别是，SLOTHY 被移出了可信计算基础。

保持诚实

形式化验证从来不是绝对的。每个证明都将形式对象——规范与模型——与非正式的现实世界需求和系统联系起来，这些联系引入了差距。形式规范是否捕捉了我们实际需要的东西？形式模型是否真实反映了实际系统？证明基础设施本身是否健全？

赢得并维护客户信任需要对这些限制保持透明。因此，我们制定并发布了一份名为 SOUNDNESS.md 的文档，其中我们指出了在 mlkem-native 中证明了什么、假设了什么以及剩余风险在哪里——从 HOL Light 证明中使用的硬件模型的保真度，到 CBMC 较大的可信计算基础，再到两个验证堆栈之间的人工桥梁。对于每个差距，我们描述了现有的缓解措施并概述了未来的工作。

我们的目标不是声称完美，而是通过透明度赢得信任。我们鼓励社区批判性地阅读 SOUNDNESS.md，挑战我们的假设，并帮助弥合剩余的差距。

上路

Mlkem-native 已集成到 AWS-LC（某机构的开源密码库）中，该库支撑着某机构服务的安全通信。集成使用一个自动导入器，直接从上游存储库拉取 mlkem-native 源代码，确保 AWS-LC 与最新的验证实现保持同步。

该集成设计为最小摩擦：mlkem-native 的模块化架构允许 AWS-LC 导入核心 ML-KEM 逻辑，同时提供其自己特定平台组件的实现。例如，AWS-LC 将 mlkem-native 的密码原语映射到其现有的 FIPS-202 (SHA-3) 实现，使用 AWS-LC 的随机数生成和内存清零功能，并在需要时启用 FIPS 模式功能，如成对一致性测试。这是一个薄薄的兼容层，将 mlkem-native 的 API 桥接到 AWS-LC 的基础设施，而无需修改经过验证的代码。

至关重要的是，证明内存安全性和类型安全性的 CBMC 契约在导入的源代码中得以保留。虽然预处理器将它们从编译后的二进制文件中移除，但它们作为代码保证的机器可检查文档保留在源代码中——一种伴随实现“活的证明”。

此外，由于 mlkem-native 和 AWS-LC 都是开源的且许可宽松，其好处超出了某机构本身。任何人都可以将 mlkem-native 集成到他们的系统中，并获得相同的性能与 assurance 组合。形式化验证工件——CBMC 契约和 HOL Light 证明——是存储库的一部分，所涉及的所有工具都是开源的，并提供了用于设置和证明检查的脚本，邀请人们独立验证我们的安全声明。

影响

Mlkem-native 的开发表明，当系统应用自动化推理时，密码工程的三个目标——安全性、性能和可维护性——并不冲突。

CBMC 使我们免于手动跟踪复杂算术中的边界，捕获那些会逃避测试并在生产环境中随机出现的错误。注释作为机器可检查的文档保留在源代码中，使代码同时更易于维护和更安全。HOL Light 和 s2n-bignum 使我们能够以正确性的数学确定性部署激进的汇编优化。SLOTHY 让我们编写清晰、可审计的代码，同时为特定微架构实现峰值性能。并且因为证明的编写与优化无关，我们可以重新定位代码而无需重做验证。

结果是一个比传统开发所能实现的更安全、更快、更易于维护的实现。我们在客户安全、客户体验和创新能力之间没有妥协：自动化推理实现了所有这三个目标。

性能对比

在 c7i（Intel Xeon Platinum 8488C）和 c7g（Graviton 3）实例上，将某机构密码库 AWS-LC 中的 ML-KEM-768 从参考实现切换到 mlkem-native 后：

• c7i：密钥生成从 30899 提升到 65146 ops/sec（2.1 倍）；封装从 30623 到 61233（2.0 倍）；解封装从 25141 到 51545（2.0 倍）。
• c7g：密钥生成从 29617 到 71134（2.4 倍）；封装从 28482 到 66874（2.3 倍）；解封装从 23919 到 64765（2.3 倍）。FINISHED