• 重要性：加密算法对在线安全至关重要，AWS 在开源加密库AWS LibCrypto（AWS-LC）中基于 Google 的 BoringSSL 项目代码实现加密算法，为 AWS 客户提供安全且针对 AWS 硬件优化的加密算法实现。
• 流行算法：x25519和Ed25519这两种加密算法基于曲线 25519 椭圆曲线越来越受欢迎，此后用 x/Ed25519 表示“x25519 和 Ed25519”。
• Graviton 芯片相关：相关内容提到 Amazon 的 Graviton2 芯片的优化提高了效率，形式验证缩短了开发时间。2023 年，AWS 在 AWS-LC 中发布了 x/Ed25519 的多个汇编级实现，通过结合自动化推理和最先进的优化技术，提高了性能并增加了正确性保证。特别针对 x86_64 和 Arm64 指令集架构，采用特定的优化方法，并尽量以恒定时间执行算法以抵御侧信道攻击。
• 椭圆曲线密码学：椭圆曲线密码学是一种公钥密码学方法，使用一对密钥，其中一个公开一个私有。曲线 25519 基于一个大质数整数，椭圆曲线具有特定性质可用于定义操作，通过椭圆曲线的标量乘法可生成公钥和私钥。
• x25519 和 Ed25519 算法：x/Ed25519 算法有不同用途，x25519 是密钥协商算法，Ed25519 是数字签名算法，已被采用于 TLS 和 SSH 等传输层协议，且在量子安全加密解决方案中也有作用。
• 微架构优化：为特定 CPU 架构编写汇编代码时使用其指令集架构（ISA），CPU 的详细实现称为微架构（μarch），不同 μarch 有独特特征。针对 x/Ed25519 算法，在不同 μarch 上进行了不同的微架构优化，如 x86_64 利用特定指令提升性能，Arm64 根据不同型号采用不同乘法算法，同时优化了所有 μarch 通用的一级操作，但二级和三级操作采用已知的最先进技术且差异不大。
• 性能结果：在 AWS Graviton 3、AWS Graviton 2 和 Intel Ice Lake 这三种 μarch 上进行测试，Ed25519 签名操作性能平均提高 108%，验证操作平均提高 37%，x25519 算法平均提高 113%，总体平均提高 86%。
• 证明正确性：在 AWS-LC 的 s2n-bignum 库中开发 x/Ed25519 实现的核心部分，并使用 HOL Light 证明其功能正确性，在汇编实现中遵循简单原则以确保证明独立于编译器，通过特定流程和工具保证算法实现的正确性，同时对 CPU 指令规范进行随机测试以提高准确性。
• 恒定时间：x/Ed25519 的实现以恒定时间为设计目标，避免因执行时间或 CPU 缓存行为依赖秘密值而导致的安全问题。
• 应用方面：AWS 广泛使用 AWS-LC 为各种服务提供加密操作，为开发者创建了与多种编程语言的绑定，目前有 Java 和 Rust 的绑定，还为 CPython 贡献了补丁，一些开源项目已在使用 AWS-LC 满足加密需求，AWS 将继续努力改进 x/Ed25519 性能和其他加密算法的优化。Torben Hansen 是 AWS 加密的应用科学家，John Harrison 是亚马逊自动化推理组的高级首席应用科学家，是 s2n-bignum 和 HOL Light 定理证明器的维护者。