椭圆曲线密码学是在线安全的核心技术。某机构在其开源密码库AWS-LC中实现了基于curve25519椭圆曲线的x25519（密钥交换）和Ed25519（数字签名）算法。通过结合自动化推理和微架构优化技术，新实现较原有版本获得显著性能提升：
核心技术优化
-
微架构级优化：
- x86_64架构：采用MULX/ADCX/ADOX指令并行处理双进位链，性能提升达30%
- Arm64架构：针对Graviton2/3不同乘法器特性，分别采用Karatsuba减法和标准教科书乘法
- 三级操作模型优化（域运算→椭圆曲线群运算→顶层运算）
-
形式化验证：
- 使用HOL Light定理证明器对s2n-bignum算术库进行机器码级验证
- 通过CI持续集成确保每次代码变更都通过形式化验证
- 对CPU指令语义进行模糊测试验证
-
时序安全：
- 恒定时序设计确保所有分支路径执行相同指令序列
- 避免使用数据依赖时序的CPU指令
性能数据
| 算法 | Graviton3提升 | Graviton2提升 | Ice Lake提升 |
|---|---|---|---|
| Ed25519签名 | 92% | 121% | 111% |
| Ed25519验证 | 28% | 43% | 40% |
| x25519密钥交换 | 131% | 97% | 111% |
应用集成
优化后的算法已集成至多语言绑定环境：
- Java（Amazon Corretto加密提供程序）
- Rust（aws-lc-rs）
- Python标准库密码学模块
该工作同时为后量子密码学混合方案提供了经典算法支撑，相关优化技术可推广至其他密码算法实现。所有代码已在AWS-LC开源库发布。
更多精彩内容 请关注我的个人公众号 公众号（办公AI智能小助手）
公众号二维码
