多项式乘法新技巧：利用单项式因子的可验证CRT多项式乘法

摘要

本文提出了一种新颖的多项式乘法变换策略，并将其应用于NTRU Prime密码系统，特别是针对在环Z4591[x]/⟨x761−x−1⟩上工作的参数集sntrup761和ntrulpr761。为了评估我们想法的实用性，我们使用ARM Neon intrinsics在C++中实现了该算法。通过进一步利用变换过程中的各种优化机会，我们在Cortex-A72上实现了最先进的性能。

由于采用了积极惰性模约简策略，溢出问题备受关注。在优化实现中，此类错误很难通过传统测试向量检测。为此，我们使用CryptoLine工具对编译后的二进制文件进行了形式化验证。我们利用了当前版本CryptoLine的所有功能，包括用于范围检查的整数集库，以及通过逻辑等价检查来验证使用最优编译器设置生成的二进制文件与使用较少优化编译生成的二进制文件等效，从而证明其正确性。

关键词

CRT多项式乘法、NTT、单项式模数、NTRU Prime

作者

• Chun-Ming Chiu（国立台湾大学，台北，台湾）
• Bo-Yin Yang（中央研究院，台北，台湾）
• Bow-Yaw Wang（中央研究院，台北，台湾）

技术细节

本文详细介绍了：

• 基于中国剩余定理（CRT）的多项式乘法新方法
• 在ARM Cortex-A72处理器上的优化实现
• 使用形式化验证工具CryptoLine确保代码正确性
• 针对NTRU Prime密码系统的具体应用

实现与验证

研究团队通过：

• 开发C++实现并利用ARM Neon指令集进行加速
• 采用惰性模约简策略提升性能
• 使用Integer Set Library进行范围检查
• 通过Logical Equivalence Checking验证编译器优化的正确性