形式化验证使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/
对网络安全、黑客技术感兴趣的朋友可以关注我的安全公众号(网络安全技术点滴分享)
公众号二维码
公众号二维码