当前位置: 首页 > news >正文

形式化验证提升RSA性能与部署效率

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

公众号二维码

公众号二维码

http://www.hskmm.com/?act=detail&tid=27444

相关文章:

  • AI元人文的硅基实现可行性Ai研究报告
  • 利用linux系统自带的cron 定时备份数据库,不需要写代码了
  • centos服务器实时备份
  • 666
  • P14150 不动鸣神,恒常乐土
  • python本地生成验证码图片
  • CentOS 7 一键安装 vsftpd 并创建可登录 FTP 用户 test - 教程
  • 【完结】-固态硬盘ssd
  • 破解工地防盗难题:如何利用国标GB28181视频平台EasyCVR实现视频监控统一管理?
  • autogen论文解读 - Sun
  • 高效仿真:功耗与散热攻略
  • Vue的nextTick函数作用
  • #6515. 「雅礼集训 2018 Day10」贪玩蓝月
  • 公告
  • 车企数据治理平台化实战:从数据孤岛到全链路治理的架构演进
  • 磁盘的管理
  • 完整教程:Java中的缓存机制与分布式缓存实现!
  • jsconfig.json-vscode或cursor ctrl点击@路径,快速到达
  • C# 弃元模式:从语法糖到性能利器的深度解析
  • 2025钣金加工厂家最新推荐榜:精密工艺与定制服务口碑之选
  • python查询数据信息,分析前了解表格结构
  • 减少磁盘延迟的方法
  • AutoCAD 2025 CAD 安装包中文永久免费免激活破解版下载 附图文安装教程
  • nmcli修改ip地址
  • 静态库与动态库:开发者必知的底层逻辑与实践技巧
  • 从C到pwn入门
  • 基于MATLAB的三轴航天器姿态控制的仿真
  • golang基础语法(四) 数组 - 教程
  • for循环s.length()-1,s为空时的一直执行循环的问题
  • 自适应工作负载的智能系统构建技术解析