Verifying Correctness of the Number Theoretic Transform and Fast Number Theoretic Transform in F⋆
As engineers continue to develop more sophisticated algorithms to optimize cryptographic algorithms, their often simple mathematical specifications become convoluted in the algorithms, from which a class of correctness bugs arise. Because cryptographic algorithms often secure sensitive information,...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Published: |
Massachusetts Institute of Technology
2024
|
| Online Access: | https://hdl.handle.net/1721.1/157189 |
| _version_ | 1824458327846813696 |
|---|---|
| author | Ono, Rick R. |
| author2 | Athalye, Anish |
| author_facet | Athalye, Anish Ono, Rick R. |
| author_sort | Ono, Rick R. |
| collection | MIT |
| description | As engineers continue to develop more sophisticated algorithms to optimize cryptographic algorithms, their often simple mathematical specifications become convoluted in the algorithms, from which a class of correctness bugs arise. Because cryptographic algorithms often secure sensitive information, their correctness, and in turn their security is a top priority. The Number Theoretic Transform (NTT) is an algorithm that enables efficient polynomial multiplication and has recently gained importance in post-quantum cryptography. This thesis presents a proof of correctness of the NTT in F⋆ , a proof-oriented programming language that extracts to OCaml, and shows that we can use the NTT to perform polynomial multiplications. We provide an implementation of the Cooley-Tukey fast NTT algorithm and a proof that it matches the original NTT specification. This thesis also presents a representation of polynomials in the F⋆ subset Low*, which extracts to performant C code. |
| first_indexed | 2025-02-19T04:24:08Z |
| format | Thesis |
| id | mit-1721.1/157189 |
| institution | Massachusetts Institute of Technology |
| last_indexed | 2025-02-19T04:24:08Z |
| publishDate | 2024 |
| publisher | Massachusetts Institute of Technology |
| record_format | dspace |
| spelling | mit-1721.1/1571892024-10-10T03:15:11Z Verifying Correctness of the Number Theoretic Transform and Fast Number Theoretic Transform in F⋆ Ono, Rick R. Athalye, Anish Zeldovich, Nickolai Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science As engineers continue to develop more sophisticated algorithms to optimize cryptographic algorithms, their often simple mathematical specifications become convoluted in the algorithms, from which a class of correctness bugs arise. Because cryptographic algorithms often secure sensitive information, their correctness, and in turn their security is a top priority. The Number Theoretic Transform (NTT) is an algorithm that enables efficient polynomial multiplication and has recently gained importance in post-quantum cryptography. This thesis presents a proof of correctness of the NTT in F⋆ , a proof-oriented programming language that extracts to OCaml, and shows that we can use the NTT to perform polynomial multiplications. We provide an implementation of the Cooley-Tukey fast NTT algorithm and a proof that it matches the original NTT specification. This thesis also presents a representation of polynomials in the F⋆ subset Low*, which extracts to performant C code. M.Eng. 2024-10-09T18:27:11Z 2024-10-09T18:27:11Z 2024-09 2024-10-07T14:34:36.025Z Thesis https://hdl.handle.net/1721.1/157189 Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0) Copyright retained by author(s) https://creativecommons.org/licenses/by-nc-nd/4.0/ application/pdf Massachusetts Institute of Technology |
| spellingShingle | Ono, Rick R. Verifying Correctness of the Number Theoretic Transform and Fast Number Theoretic Transform in F⋆ |
| title | Verifying Correctness of the Number Theoretic Transform and Fast Number Theoretic Transform in F⋆ |
| title_full | Verifying Correctness of the Number Theoretic Transform and Fast Number Theoretic Transform in F⋆ |
| title_fullStr | Verifying Correctness of the Number Theoretic Transform and Fast Number Theoretic Transform in F⋆ |
| title_full_unstemmed | Verifying Correctness of the Number Theoretic Transform and Fast Number Theoretic Transform in F⋆ |
| title_short | Verifying Correctness of the Number Theoretic Transform and Fast Number Theoretic Transform in F⋆ |
| title_sort | verifying correctness of the number theoretic transform and fast number theoretic transform in f⋆ |
| url | https://hdl.handle.net/1721.1/157189 |
| work_keys_str_mv | AT onorickr verifyingcorrectnessofthenumbertheoretictransformandfastnumbertheoretictransforminf |