性能更优的“25519”椭圆曲线密码算法
通过结合自动推理和针对CPU微架构的优化，既提升了性能，也增强了正确实现的保障。
作者：Torben Hansen, John Harrison
2024年9月10日
密码算法对于在线安全至关重要。在亚马逊云服务（AWS），我们在开源的密码库AWS LibCrypto（AWS-LC）中实现了多种密码算法，该库基于谷歌的BoringSSL项目代码。AWS-LC为AWS客户提供了安全且针对AWS硬件优化的密码算法实现。
x25519和Ed25519这两种密码算法日益流行，它们都基于一条名为curve25519的椭圆曲线。为了改善客户在使用这些算法时的体验，我们最近对它们在AWS-LC中的实现进行了更深入的研究。下文将使用x/Ed25519作为“x25519和Ed25519”的简称。
2023年，AWS在AWS-LC中发布了多个针对x/Ed25519的汇编级实现。通过结合自动推理和最先进的优化技术，这些新实现不仅比原有的AWS-LC实现性能更优，还增强了其正确性的保障。
具体来说，我们使用自动推理证明了功能正确性，并针对x86_64和Arm64指令集架构下的特定CPU微架构采用了优化技术。同时，我们尽最大努力确保算法以常量时间执行，以抵御通过计算时长推断秘密信息的旁路攻击。
在本文中，我们将探讨这项工作的不同方面，包括通过自动推理证明正确性的流程、微架构优化技术、编写常量时间代码的特殊考量，以及性能提升的量化评估。
椭圆曲线密码学
椭圆曲线密码学是一种实现公钥密码的方法，它使用一对密钥：一个公钥和一个私钥。最著名的公钥密码方案之一是RSA，其公钥是一个非常大的整数，而对应的私钥是该整数的质因数。RSA方案既可用于数据加密/解密，也可用于数据签名/验证。
椭圆曲线为数学关联公钥和私钥提供了另一种方式，有时，这意味着我们可以更高效地实现密码方案。尽管椭圆曲线的数学理论既广泛又深奥，但密码学中使用的椭圆曲线通常由形式为 y² = x³ + ax² + bx + c 的方程定义，其中a、b、c是常数。可以将满足方程的点绘制在二维图形上。
椭圆曲线有一个特性：一条与曲线相交于两点的直线，最多与曲线相交于另一点。这个特性被用于定义曲线上的运算。例如，曲线上两点的加法并非直接定义为与这两点共线的第三个点，而是该第三点关于对称轴的反射点。
现在，如果曲线上的点坐标对某个整数取模，曲线就变成了平面上的一个散点集合，但这个集合仍然具有对称性，因此加法运算仍然有效。Curve25519以一个大的质数命名，具体来说是 2²⁵⁵ - 19。模curve25519质数的数集，连同基本的算术运算（例如两个数模该质数的乘法），定义了执行椭圆曲线运算的域。
连续执行椭圆曲线加法被称为标量乘法，其中的标量就是加法的次数。在密码学使用的椭圆曲线中，如果你只知道标量乘法的结果，而标量足够大，那么反推出标量在计算上是不可行的。标量乘法的结果成为公钥的基础，原始标量则成为私钥的基础。
x25519 和 Ed25519 密码算法
x/Ed25519 算法各有不同的用途。x25519 是一种密钥协商算法，用于在两个对等方之间安全地建立共享密钥；Ed25519 是一种数字签名算法，用于对数据进行签名和验证。
x/Ed25519 算法已被 TLS 和 SSH 等传输层协议采用。2023 年，NIST 宣布更新其 FIPS185-6 数字签名标准，其中就包括增加了 Ed25519。x25519 算法在后量子安全密码解决方案中也扮演着重要角色，它作为经典算法已被纳入 TLS 1.3 和 SSH 混合方案规范中，用于后量子密钥协商。
微架构优化
当我们为特定 CPU 架构编写汇编代码时，我们使用的是其指令集架构。ISA 定义了可用汇编指令、指令语义以及程序员可访问的 CPU 寄存器等资源。重要的是，ISA 是从抽象层面定义 CPU，它并不规定 CPU 应如何在硬件中实现。
CPU 的详细实现称为微架构，每个微架构都有其独特的特性。例如，尽管 AWS Graviton 2 CPU 和 AWS Graviton 3 CPU 都基于 Arm64 ISA，但它们的微架构实现是不同的。我们假设，如果能利用这些微架构差异，我们就能创建比 AWS-LC 中现有实现更快的 x/Ed25519 实现。事实证明，这个直觉是正确的。
让我们仔细看看我们是如何利用微架构差异的。在 curve25519 上可以定义不同的算术运算，这些运算的不同组合被用来构建 x/Ed25519 算法。从逻辑上讲，必要的算术运算可以在三个层面上考虑：
- 域运算：在由 curve25519 质数 2²⁵⁵ - 19 定义的域内的运算。
- 椭圆曲线群运算：应用于曲线元素本身的运算，例如两个点 P1 和 P2 的加法。
- 顶层运算：通过迭代应用椭圆曲线群运算实现的运算，例如标量乘法。
每个层面都有自己的优化途径。我们将依赖于微架构的优化重点放在第一层的运算上，而对于第二层和第三层，我们的实现采用了已知的最先进技术，并且在不同的微架构上基本相同。下面，我们总结了在 x/Ed25519 实现中做出的不同依赖于微架构的选择。
对于现代 x86_64 微架构，我们使用了 MULX、ADCX 和 ADOX 指令，它们是标准汇编指令 MUL（乘法）和 ADC（带进位加法）的变体，常见于通常称为 BMI 和 ADX 的指令集扩展中。这些指令的特殊之处在于，当组合使用时，它们可以并行维护两个进位链，据观察，这可以将性能提升高达 30%。对于不支持这些指令集扩展的较老 x86_64 微架构，我们使用更传统的单进位链。
对于 Arm64 微架构，例如具有改进的整数乘法器的 AWS Graviton 3，我们使用了相对直接的教科书式乘法，事实证明这能带来良好的性能。AWS Graviton 2 的乘法器较小。对于这种 Arm64 微架构，我们使用了 Karatsuba 乘法的减法形式，它可以递归地分解乘法运算。原因在于，在这些微架构上，产生 128 位结果的 64x64 位乘法相对于其他运算的吞吐量要低得多，这使得 Karatsuba 优化变得有价值的数值规模小得多。
我们还优化了所有微架构通用的第一层运算。一个例子涉及使用二进制最大公约数算法来计算模逆元。我们使用了二进制GCD的“divstep”形式，它有利于高效实现，但这也给我们的第二个目标——正式证明正确性——带来了复杂性。
性能结果
在本节中，我们将重点展示性能的提升。为简洁起见，我们仅关注三种微架构：AWS Graviton 3、AWS Graviton 2 和 Intel Ice Lake。为了收集性能数据，我们使用了具有匹配 CPU 微架构的 EC2 实例——分别是 c6g.4xlarge、c7g.4xlarge 和 c6i.4xlarge；为了测量每个算法，我们使用了 AWS-LC 速度工具。
在下面的图表中，所有单位均为每秒操作数。优化前列代表 AWS-LC 中现有 x/Ed25519 实现的性能。优化后列代表新实现的性能。
对于 Ed25519 签名操作，在三种微架构上，新实现的每秒操作数平均提高了 108%。
对于 Ed25519 验证操作，在三种微架构上，新实现的每秒操作数平均提高了 37%。
我们观察到 x25519 算法的改进最大。注意，下图中一个 x25519 操作包括了 x25519 密钥交换协议所需的两个主要操作：基点乘法和变点乘法。
对于 x25519，在三种微架构上，新实现的每秒操作数平均提高了 113%。
平均而言，在 AWS Graviton 2、AWS Graviton 3 和 Intel Ice Lake 微架构上，我们看到了 86% 的性能提升。
正确性证明
我们在 AWS-LC 中开发的 x/Ed25519 实现的核心部分位于 s2n-bignum 中，这是一个 AWS 自有的整数算术例程库，专为密码应用而设计。在 s2n-bignum 库中，我们也使用 HOL Light 证明了这些实现的功能正确性。HOL Light 是一个用于高阶逻辑的交互式定理证明器，其设计目标是采用一种特别简单（因此称为 light）的“正确性内建”的证明方法。这种简单性提供了保证：任何“被证明”的东西都确实是经过严格证明的，而不是证明器缺陷的产物。
在编写汇编实现时，我们也遵循同样的简单性原则。用汇编编写更具挑战性，但在证明正确性时，它提供了一个明显的优势：我们的证明变得独立于任何编译器。
下图展示了我们用于证明 x/Ed25519 正确性的流程。该流程需要两组不同的输入：第一组是我们正在评估的算法实现；第二组是一个证明脚本，它模拟了算法的正确数学行为以及 CPU 的行为。证明是由一系列特定于 HOL Light 的函数组成的序列，这些函数代表了证明策略及其应用顺序。编写证明并非自动化，需要开发人员的独创性。
根据算法实现和证明脚本，HOL Light 要么确定该实现是正确的，要么在无法确定时失败。HOL Light 将算法实现视为一系列机器代码字节。通过使用提供的 CPU 指令规范以及证明脚本中由开发人员编写的策略，HOL Light 推理执行过程的正确性。
这部分正确性证明是自动化的，我们甚至在 s2n-bignum 的持续集成工作流中实现了它。CI 覆盖的工作流在下图中用红色虚线突出显示。CI 集成提供了一种保障：任何对算法实现代码的更改，如果没有成功通过正式的正确性证明，都无法提交到 s2n-bignum 的代码仓库。
CPU 指令规范是我们正确性证明中最关键的要素之一。为了使证明在实践中成立，该规范必须捕捉每条指令在真实世界中的语义。为了提高这方面的保证，我们在真实硬件上对指令规范进行了随机化测试，以“模糊测试”的方式排除不准确之处。
常量时间
我们在设计和实现优化时，将安全性作为首要考量。密码代码必须努力避免侧信道漏洞，这些漏洞可能允许未经授权的用户提取私密信息。例如，如果密码代码的执行时间依赖于秘密值，那么就有可能通过执行时间来推断这些值。同样，如果 CPU 缓存行为依赖于秘密值，共享缓存的未经授权用户就可能推断出这些值。
我们的 x/Ed25519 实现在设计时考虑到了常量时间的要求。无论输入值如何，它们都执行完全相同的基本 CPU 指令序列，并避免任何可能具有数据依赖时序的 CPU 指令。
在应用中运用 x/Ed25519 优化
AWS 在众多不同的 AWS 服务子系统中广泛使用 AWS-LC 来驱动密码运算。您可以通过在您的应用程序中使用 AWS-LC，来利用本文介绍的 x/Ed25519 优化。请访问 Github 上的 AWS-LC 以了解更多关于如何将 AWS-LC 集成到您的应用程序中的信息。
为了便于开发者集成，AWS 为多种编程语言创建了从 AWS-LC 到这些语言的绑定。这些绑定通过定义良好的 API 公开 AWS-LC 中的密码功能，免除了在高级编程语言中重新实现密码算法的需要。目前，AWS 已开源了 Java 和 Rust 的绑定——用于 Java 的 Amazon Corretto 加密提供程序，以及用于 Rust 的 AWS-LC。此外，我们还贡献了补丁，允许 CPython 基于 AWS-LC 构建，并将其用于 Python 标准库中的所有密码学操作。下面我们重点介绍一些已经使用 AWS-LC 来满足其密码需求的开源项目。
我们的工作尚未结束。我们将继续努力提高 x/Ed25519 的性能，并持续探索 s2n-bignum 和 AWS-LC 支持的其他密码算法的优化。请关注 s2n-bignum 和 AWS-LC 的代码仓库以获取最新更新。FINISHED
