形式化验证加速RSA性能与部署

形式化验证使RSA更快——且部署更迅速

某中心Graviton2芯片的优化提升效率，形式化验证缩短开发时间。

大多数在线安全交易受RSA等公钥加密方案保护，其安全性基于大数分解的难度。公钥加密通过支持私钥的加密交换提升安全性，但由于依赖大整数模幂等操作，会带来显著计算开销。研究人员和工程师引入各种优化以提高公钥加密效率，但由此产生的复杂性使得验证加密算法行为正确变得困难。加密算法中的错误可能导致灾难性后果。

本文阐述某中心自动推理团队如何通过结合形式化验证，在某中心Graviton2芯片上将RSA签名吞吐量提升33%至94%（取决于密钥大小），同时证明优化方案的功能正确性。

Graviton2架构背景

Graviton2是基于Arm Neoverse N1内核的服务器级CPU。为提升RSA签名吞吐量，结合了快速模算术技术与Graviton2特定的汇编级优化。代码采用恒定时间风格编写（例如无秘密相关分支或内存访问模式）以避免侧信道攻击。优化函数及其证明已纳入某机构Web服务的s2n-bignum形式化验证大数运算库，并被AWS-LC密码库及其绑定项目采用。

性能提升数据

步骤一：Graviton2上的RSA加速优化

算法优化

• 蒙哥马利模乘法：将数字表示为蒙哥马利形式，提升模运算序列效率。
• Karatsuba算法：将乘法分解为三个较小乘法，针对2048和4096位密钥实现31-49%加速，3072位仍使用二次乘法。
• 平方专用函数：针对操作数相等的情况进一步优化。

微架构优化

• SIMD向量化：利用Neon SIMD扩展，将标量64位乘法向量化，通过并行执行提升效率。
• 向量化策略：枚举不同向量化代码并计时执行，选择最优方案。
• 寄存器数据传输：通过双内存加载避免管道冲突，优化数据移动。
• 恒定时间查表：重新实现向量化恒定时间查找表，结合前期优化实现80-94%加速。

指令调度

• 手动调度指令以利用乱序执行特性。
• 探索SLOTHY超优化器自动调度，实现95-120%吞吐量提升，但因验证挑战暂未集成至生产环境。

步骤二：代码形式化验证

s2n-bignum框架

• 集成了x86-64和Arm汇编代码的形式化验证框架。
• 每个汇编函数具有功能正确性规范，包括前置条件、后置条件和状态变更约束。

HOL Light定理证明

• 使用符号执行和Floyd-Hoare逻辑中间注解策略验证代码。
• 通过抽象化简化符号模拟，确保数学模型与硬件行为一致。

未来改进方向

• 当前验证未覆盖非功能属性（如侧信道泄漏）。
• 通过禁用可变时序指令和秘密相关分支实现防护。
• 正在探索形式化验证信息泄漏缺失的方法。