企业官网建设流程全解析

手机电视直播网站大全,网络公司网站建,好看的企业网站模板,汕头网站安全开发系统在线安全交易大多由RSA等公钥加密方案保护#xff0c;其安全性基于大数分解的难度。公钥加密通过实现私钥的加密交换来提高安全性#xff0c;但由于依赖于大整数模幂运算等操作#xff0c;会带来显著的计算开销。 研究人员和工程师引入了各种优化来提高公钥加密的效率#…在线安全交易大多由RSA等公钥加密方案保护其安全性基于大数分解的难度。公钥加密通过实现私钥的加密交换来提高安全性但由于依赖于大整数模幂运算等操作会带来显著的计算开销。研究人员和工程师引入了各种优化来提高公钥加密的效率但由此产生的复杂性使得验证加密算法是否正确运行变得困难。加密算法中的漏洞可能是灾难性的。本文阐释了某中心的自动推理小组如何将某中心Graviton2芯片上的RSA签名吞吐量提高了33%至94%取决于密钥大小同时使用形式化验证证明了优化的功能正确性。Graviton2上的RSA优化Graviton2是基于Arm Neoverse N1内核的服务器级CPU。为了提高Graviton2上RSA签名的吞吐量我们将多种快速模算术技术与针对Graviton2的汇编级优化相结合。算法优化为了进行快速、安全的模算术蒙哥马利模乘法是一种广泛应用的技术。我们在实现蒙哥马利乘法时将其分解为大整数乘法和一个单独的蒙哥马利约减步骤。在Graviton2上这种方法的好处在于我们可以使用著名的Karatsuba算法用成本较低的加法操作来换取昂贵的乘法操作。Karatsuba算法将一次乘法分解为三次较小的乘法并结合一些寄存器移位操作。它可以递归执行对于大数运算比标准乘法算法更高效。我们对2,048位和4,096位等2的幂次比特大小使用了Karatsuba算法。对于其他大小如3072位我们仍然使用二次乘法。当两个操作数相等时Karatsuba乘法可以进一步优化我们还专门编写了平方运算函数。通过这些优化与原始代码相比我们在2,048位和4,096位RSA签名上实现了31-49%的速度提升。微架构优化许多Arm CPU实现了Neon单指令多数据架构扩展。它增加了一组128位寄存器这些寄存器被视为各种大小8/16/32/64位的向量以及可以并行操作这些向量的SIMD指令。此外SIMD指令使用与标量指令不同的流水线因此两种指令可以并行执行。向量化策略使用SIMD指令我们将标量64位乘法向量化。对于大整数乘法向量化的64位低位乘法代码与标量64位高位乘法指令很好地重叠。对于平方运算向量化两个64×64→128位的平方运算效果很好。对于蒙哥马利约减中的乘法向量化64×64→128位乘法和64×64→64低位乘法是有效的。我们通过脚本枚举不同向量化的代码并计时执行来选择向量化的具体方案。快速恒定时间查表代码另一项独立改进是重新实现了用于快速模幂运算算法的向量化恒定时间查找表。结合之前的优化与初始代码的吞吐量相比我们在2,048/4,096位RSA签名上实现了80-94%的速度提升在3,072位签名上实现了33%的速度提升。指令调度尽管Graviton2是乱序执行CPU但由于重排序缓冲区和发射队列等组件的容量有限仔细调度指令对性能仍然很重要。我们通过手动指令调度获得了良好的结果。我们还研究了使用基于约束求解和简化微架构模型的SLOTHY超级优化器来自动化此过程。通过对蒙哥马利约减进行额外调整以预计算Karatsuba中使用的一些数字SLOTHY优化使得2,048/4,096位吞吐量提升了95-120%3,072位提升了46%。然而由于验证自动调度具有挑战性此方法尚未集成到相关库中。使用形式化验证确保代码正确性为了将优化后的代码部署到生产环境我们需要确保其正确运行。随机测试是快速检查简单和已知情况的廉价方法但要提供更高水平的保证我们依赖于形式化验证。s2n-bignum库简介某机构的s2n-bignum库既是一个用于形式化验证x86-64和Arm汇编代码的框架也是一个使用该框架验证的快速加密汇编函数集合。s2n-bignum中的规范s2n-bignum中的每个汇编函数都有一个说明其功能正确性的规范。规范表明对于满足某些前提条件的任何程序状态程序的输出状态必须满足某些后置条件。使用HOL Light验证汇编为了证明实现相对于规范是正确的我们使用HOL Light交互式定理证明器。s2n-bignum使用两种策略的组合来验证程序符号执行给定使用符号变量代替具体值的输入程序状态表示符号执行在代码片段的末尾推断出一个符号输出状态实质上进行了一种更严格和更通用的程序执行形式。基于Floyd-Hoare逻辑风格的中间标注每个中间断言既是前一段代码的后置条件也是后一段代码的前提条件。断言只需包含证明其相应后置条件所需的细节。这种抽象有助于使符号模拟更易于处理。我们假设Arm硬件的运行符合s2n-bignum的模型但该模型是精心开发的并通过与硬件进行广泛的交叉检查验证了其解释。未来形式化验证的改进s2n-bignum的形式化验证尚未涵盖实现的非功能性属性包括其是否可能通过诸如代码运行时间等侧信道泄露信息。相反我们通过严格的通用实现风格来处理这个问题从不使用具有可变执行时间的指令如除法并且没有依赖于秘密数据的条件分支/内存访问模式。此外我们使用简单的静态检查来验证其中一些属性并在具有广泛不同比特密度的输入上执行代码以分析相应的运行时间并调查任何意外的相关性。这些规范和健全性检查是我们的标准实践我们将其应用于本文描述的所有新实现。在正在进行的工作中我们正在探索正式验证信息无泄漏的可能性。更多精彩内容 请关注我的个人公众号 公众号办公AI智能小助手或者 我的个人博客 https://blog.qife122.com/对网络安全、黑客技术感兴趣的朋友可以关注我的安全公众号网络安全技术点滴分享