形式化验证使RSA更快——部署也更迅速
大多数在线安全交易都受到RSA等公钥加密方案的保护，其安全性依赖于大数分解的难度。公钥加密通过实现私钥的加密交换来提高安全性，但由于依赖大整数模幂运算等操作，会带来显著的计算开销。
研究人员和工程师引入了各种优化来提高公钥加密效率，但由此产生的复杂性使得难以验证加密算法是否正常运行。加密算法中的错误可能是灾难性的。
Graviton2芯片上的RSA优化
Graviton2是基于Arm Neoverse N1核心的服务器级CPU。为了提高Graviton2上RSA签名的吞吐量，我们结合了快速模算术的各种技术与特定于Graviton2的汇编级优化。为了证明优化代码的功能正确性，我们使用HOL Light交互式定理证明器对其进行了形式化验证。
我们的代码以恒定时间风格编写（例如，没有秘密相关的分支或内存访问模式），以避免侧信道攻击。优化函数及其证明包含在s2n-bignum正式验证的大数运算库中。
| 密钥大小（位） | 基线吞吐量（操作/秒） | 改进后吞吐量（操作/秒） | 加速比（%） |
|---|---|---|---|
| 2048 | 299 | 541 | 81.00% |
| 3072 | 95 | 127 | 33.50% |
| 4096 | 42 | 81 | 94.20% |
第一步：使RSA在Graviton2上快速运行
算法优化
对于快速安全的模算术，蒙哥马利模乘法是一种广泛使用的技术。我们在Graviton2上实现蒙哥马利乘法为大整数乘法和单独的蒙哥马利约减的组合。
对于Graviton2，这种方法的优势是我们可以使用著名的Karatsuba算法，用加法操作替代昂贵的乘法。Karatsuba算法将乘法分解为三个较小的乘法，以及一些寄存器移位。它可以递归执行，对于大数来说比标准乘法算法更高效。
我们针对2,048位和4,096位等2的幂次位大小使用了Karatsuba算法。通过这些优化，与原始代码相比，我们在2,048位和4,096位RSA签名中实现了31-49%的加速。
微架构优化
许多Arm CPU实现了Neon单指令多数据（SIMD）架构扩展。它增加了一组128位寄存器，这些寄存器被视为各种大小（8/16/32/64位）的向量，以及可以并行操作这些向量的SIMD指令。
向量化策略：使用SIMD指令，我们将标量64位乘法向量化。对于大整数乘法，向量化的64位乘低代码与标量64位乘高指令（UMULH）很好地重叠。对于平方运算，向量化两个64×64→128位平方运算效果良好。
快速恒定时间查找表代码：另一个独立改进是重新实现了向量化恒定时间查找表，用于快速模幂算法。结合我们之前的优化，与我们初始代码的2,048/4,096位RSA签名吞吐量相比，进一步将加速比提高到80-94%，3,072位签名也有33%的加速。
指令调度：尽管Graviton2是乱序CPU，但由于重排序缓冲区和发射队列等组件的有限容量，仔细调度指令对性能很重要。我们还研究了使用基于约束求解和（简化的）微架构模型的SLOTHY超级优化器自动化该过程。
第二步：正式验证代码
为了在生产中部署优化代码，我们需要确保其正常工作。随机测试是快速检查简单和已知情况的廉价方法，但为了提供更高级别的保证，我们依赖形式化验证。
s2n-bignum简介
s2n-bignum既是用于正式验证x86-64和Arm中汇编代码的框架，也是使用该框架本身正式验证的密码学快速汇编函数集合。
s2n-bignum中的规范：s2n-bignum中的每个汇编函数（包括RSA中使用的新汇编函数）都有一个说明其功能正确性的规范。规范规定，对于满足某些前提条件的任何程序状态，程序的输出状态必须满足某些后置条件。
使用HOL Light验证汇编：为了证明实现相对于规范是正确的，我们使用HOL Light交互式定理证明器。与"黑盒"自动定理证明器相比，像HOL Light这样的工具强调自动化常规证明步骤与允许明确的、可编程的用户指导之间的平衡。
s2n-bignum使用两种策略的组合来验证程序：
- 符号执行：使用符号变量代替特定值表示输入程序状态，符号执行在代码片段的末尾推断出符号输出状态
- Floyd-Hoare逻辑风格的中间注释：每个中间断言作为前面代码的后置条件和后续代码的前提条件
未来形式化验证改进
s2n-bignum的形式化验证尚未涵盖实现的非功能属性，包括是否可能通过侧信道（如代码运行时间）泄漏信息。我们通过有纪律的通用实现风格来处理这个问题：从不使用具有可变时序的指令，也没有依赖于秘密数据的条件分支/内存访问模式。
这些纪律和健全性检查是我们的标准实践，我们将其应用于此处描述的所有新实现。在正在进行的工作中，我们正在探索正式验证信息不泄漏的可能性。
更多精彩内容 请关注我的个人公众号 公众号（办公AI智能小助手）或者 我的个人博客 https://blog.qife122.com/
对网络安全、黑客技术感兴趣的朋友可以关注我的安全公众号（网络安全技术点滴分享）
公众号二维码
公众号二维码
