多項式乘法的新技巧：驗證應用單項式於中國剩餘定理之多項式乘法

Abstract

針對多項式乘法的問題，我們在論文中展示了新穎的轉換策略，並示範如何將其應用在 NTRU Prime 密碼系統上。明確而言，在此密碼系統的所有參數集中，我們特別關注了 sntrup761 跟 ntrulpr761 這兩者。它們使用的多項式商環都是 ℤ₄₅₉₁[x]/⟨x⁷⁶¹−x−1⟩。為了評估我們的新想法是否具實用性，我們使用了 C++ 語言與 ARM Neon intrinsics，將新提出的演算法實做出來。過程中我們發現到，代數轉換過程中事實上存在著不少優化契機。我們進一步利用了這些機會，最終設計出了效率十分出色的乘法器，其在 Cortex-A72 的平台上的計算速度勝過了所有現有紀錄。 通常而言，為了避免整數溢流錯誤，基於整數模運算的演算法會經常需要更換計算過程的中間值，轉而用另一個同餘但絕對值較小的整數取代。為了追求效率，我們在實做中盡可能跳過了這個步驟。不可否認的，這增加了整數溢流錯誤的危險性。針對這類型的錯誤，由於引發機率實在過低，基於測試資料的傳統偵測方法往往是沒有幫助的。為了確認我們實做出的是否正確無誤，我們運用了名為 CryptoLine 的形式驗證工具。驗證過程中，我們使用了 CryptoLine 最新版本的所有功能，其中幫助最大的兩個功能是基於 Integer Set Library 的值域驗證，以及程式等價性的驗證。透過後者，我們可以將同一個程式碼用不同的設定，編譯成另一個「優化較不徹底但容易驗證」的執行檔。最終透過證明新版本的正確性以及兩者的等價性，我們可以間接得到原版本執行檔的正確性保證。

In this paper we present a novel transformation strategy for polynomial multiplications and apply it to NTRU Prime, specifically the parameter sets sntrup761 and ntrulpr761 working in the ring ℤ₄₅₉₁[x]/⟨x⁷⁶¹−x−1⟩. To evaluate the practicality of our idea, we implemented the algorithm in C++ with ARM Neon intrinsics. By further exploiting the various optimization opportunities in the transformation process, we achieve state-of-the-art performance on Cortex-A72. Because of the aggressively lazy modular reduction strategy, overflows are of serious concern. Such errors in an optimized implementation are notoriously difficult to detect using traditional test vectors. To this end, the compiled binary file is formally verified using the tool CryptoLine. We use all the features in the current version of CryptoLine. This includes the Integer Set Library for range checking, plus the Logical Equivalence Checking to verify the correctness of the binary produced with the most optimized compiler setting by showing it as being equivalent to a binary from a less optimized compilation.