主要观点：

• 多数在线安全交易受 RSA 等公钥加密方案保护，其安全性依赖大数分解难度，但引入计算开销。
• 研究人员和工程师引入多种优化使公钥加密更高效，但验证算法正确性困难，加密算法漏洞可能很严重。
• 亚马逊自动化推理小组将 RSA 签名在 Graviton2 芯片上的吞吐量提高了 33% - 94%，并使用形式验证证明优化的功能正确性。

关键信息：

• Graviton2 是基于 Arm Neoverse N1 核心的服务器级 CPU，亚马逊自动化推理小组结合多种技术和优化来提高 RSA 签名吞吐量。
• 算法优化方面，采用 Montgomery 模乘法，对不同位大小使用不同乘法算法（如 2048 位和 4096 位用 Karatsuba 算法），实现了 31 - 49%的加速。
• 微架构优化方面，利用 Neon SIMD 架构扩展进行向量化，通过精心安排指令、优化常量时间表查找代码和指令调度等方式进一步提高性能，SLOTHY 优化使 2048/4096 位吞吐量提高 95 - 120%，3072 位提高 46%。
• 为确保优化代码正确运行，使用形式验证，以 AWS 的 s2n-bignum 框架验证 RSA 新汇编函数的功能正确性，通过符号执行和中间注释等策略，假设 Arm 硬件符合模型并进行验证，同时正在探索验证无信息泄露的可能性。

重要细节：

• 64 位 Arm CPU 上乘法指令的延迟和流水线停顿情况，以及在 Graviton2 上的优化措施。
• 向量化策略的具体实现，包括不同操作的向量化方式和选择向量化的 scalar 乘法的方法。
• s2n-bignum 中每个汇编函数的规格说明，包括输入和输出状态的条件及关系。
• HOL Light 交互式定理证明器的使用，以及符号执行和中间注释等验证策略。