Implementation and Verification of a FIPS 203-Compatible Number Theoretic Transform on a Field-Programmable Gate Array

Abstract

This thesis aims to implement the Number Theoretic Transform (NTT) optimization used in Module-Lattice-Based Key-Encapsulation Mechanism (ML-KEM) for polynomial multiplication on a Field Programmable Gate Array (FPGA). An additional aim is to verify the correct functionality of the implementation, through formal verification methods. The ML-KEM scheme was standardized by NIST in FIPS 203, after a public post-quantum cryptography (PQC) competition to answer the threat that quantum computers cause against traditional asymmetric cryptography. ML-KEM is widely deployed and recommended for use in a hybrid manner alongside established asymmetric cryptography.

The theoretic background on FPGAs, lattice cryptography, NTT, and formal verification for hardware is introduced. Lattice cryptography and NTT are approached from the view of their role in ML-KEM. The ML-KEM scheme is described, including how its IND-CPA public-key encryption (PKE) scheme is transformed into an IND-CCA2 key-encapsulation mechanism (KEM) through the Fujisaki-Okamoto transform.

The implemented design performs the NTT operations described in FIPS 203. However, it is slow compared to the designs in literature. Additionally, the coverage of formal verification ended up lacking, and it was supplemented with simulation-based verification instead.

Tämän diplomityön tavoitteena on toteuttaa ML-KEM-avaintenkapselointimekanismin polynomikertolaskussa käytetty lukuteoreettiseen muunnokseen perustuva optimointi ohjelmoitavalle porttimatriisille. Lisäksi tavoitteena on varmistaa toteutuksen oikea toiminnallisuus formaalin verifioinnin menetelmin. NIST standardoi ML-KEM:in FIPS 203 -julkaisussa kvanttiturvallisten algoritmien kilpailun tuloksena, vastauksena kvanttitietokoneiden klassisille julkisen avaimen kryptografian menetelmille aiheuttamaan uhkaan. ML-KEM on laajalti käytössä ja suositeltu käytettäväksi hybridimenetelmässä vakiintuneiden julkisen avaimen algoritmien rinnalla.

Työssä esitellään teoreettinen tausta ohjelmoitavista porttimatriiseista, hilakryptografiasta, lukuteoreettisestä muunnoksesta sekä laitteiston formaalista verifioinnista. Hilakryptografiaa ja lukuteoreettista muunnosta lähestytään niiden roolin kautta ML-KEM:issä. Työssä kuvataan ML-KEM, sekä kuinka sen IND-CPA-julkisen avaimen salausmenetelmä muunnetaan IND-CCA2-avaintenkapselointimekanismiksi Fujisaki-Okamoto-muunnoksen avulla.

Toteutus suorittaa FIPS 203:ssa määritellyt lukuteoreettisen muunnoksen operaatiot. Se on kuitenkin kirjallisuuden toteutuksiin verrattuna hidas. Lisäksi formaalin verifioinnin kattavuus jäi puutteelliseksi, ja sitä täydennettiin simulaatiopohjaisella verifioinnilla.