Verification of an Optimized NTT Algorithm.

The Number Theoretic Transform (NTT) is an efficient algorithm for computing products of polynomials with coefficients in finite fields. It is a common procedure in lattice-based key-exchange and signature schemes. These new cryptographic algorithms are becoming increasingly important because they are quantum resistant . No quantum algorithm is known to break these lattice-based algorithms, unlike older schemes such as RSA or elliptic curve cryptosystems. Many implementations and optimizations of the NTT have been proposed in the literature. A particular efficient variant is due to Longa and Naehrig. We have implemented several of these variants, including an improved version of the Longa and Naehrig algorithm. An important concern is to show that numerical overflows do not happen in such algorithms. We report on several attempts at automatically verifying the absence of overflows using static analysis tools. Off-the-shelf tools do not work on the NTT code. We present a specialized abstract-interpretation method to solve the problem.