Verified NTT Multiplications for NISTPQC KEM Lattice Finalists: Kyber, SABER, and NTRU

This artifact contains the source code of CryptoLine and benchmarks to
reproduce the results from our paper "Verified NTT Multiplications
for NISTPQC KEM Lattice Finalists: Kyber, SABER, and NTRU" in CHES
2022.
The experiments in the paper run on a Ubuntu 20.04.3 server with
3.2GHz Intel Xeon (with 32 logical cores) and 1TB RAM.
All the 32 CPU cores are used during the experiments.
The minimum requirements for running the experiments are 256GB RAM
and 5GB free disk space.
Scripts provided in this artifact may not work on other Ubuntu
versions or other Linux distributions.

Prerequisite

To compile CryptoLine and run the experiments, the following packages
need to be installed.

• sudo
• bc
• OCaml compiler (version 4.08.1 up)
• GNU Make
• OCaml packages: dune, ocamlfind, lwt, lwt_ppx, zarith
• The computer algebra system Singular
• The SMT QF_BV solver Boolector

CryptoLine is successfully compiled with OCaml 4.08.1, 4.11.2,
4.12.1, 4.13.1, and 4.14.0 together with dune 3.2.0, lwt 5.5.0,
lwt_ppx 2.0.3, and zarith 1.12.

All the required packages except sudo can be installed via the script
build.sh provided in this artifact.
To run build.sh, make sure that sudo is already installed and the
user running build.sh is in the group sudo.

Installation

Follow the following instructions (or simply run the script build.sh
in the project root) to build and install CryptoLine as well as
the compute algebra system Singular and the SMT QF_BV solver Boolector
on Ubuntu 20.04 LTS.

$ sudo apt -y install \
    build-essential bc ocaml ocaml-dune libzarith-ocaml-dev \
    liblwt-ocaml-dev
$ scripts/install-singular.sh
$ scripts/install-boolector.sh
$ dune build
$ sudo dune install

Run the following command to see the available command-line arguments.

$ cv -help

To uninstall CryptoLine, run the following command.

$ sudo dune uninstall

CHES2022 Experiments

Experiment: Table 3

To run the experiment of verifying the Intel AVX2 and Cortex-M4
assembly implementations for the NTTs for Kyber, NTRU, and Saber (see
Table 3 in the paper), run the script
ches2022_run_experiments_table3.sh in the project root.

$ ./ches2022_run_experiments_table3.sh

This experiment uses 32 CPU cores and the running time is around 1 day
on our server.
The CryptoLine specifications of the assembly implementations are
listed below.

• Kyber768
  • AVX2
    • Normal: examples/ches2022/kyber768/avx2/PQCLEAN_KYBER768_AVX2_polyvec_ntt.cl
    • Inverse: examples/ches2022/kyber768/avx2/PQCLEAN_KYBER768_AVX2_polyvec_invntt_tomont2.cl
  • Cortex-M4
    • Normal: examples/ches2022/kyber768/pqm4/ntt_fast.cl
    • Inverse: examples/ches2022/kyber768/pqm4/invntt_fast_tuned.cl
• ntru2048509
  • AVX2
    • Normal: examples/ches2022/ntruhps2048509/avx2/nttmul_poly_ntt.cl
    • Inverse: examples/ches2022/ntruhps2048509/avx2/nttmul_poly_invntt_tomont2.cl
  • Cortex-M4
    • Normal:
      • examples/ches2022/ntruhps2048509/pqm4/__asm_ntt_0_1_2_3_32.cl
      • examples/ches2022/ntruhps2048509/pqm4/__asm_ntt_4_5_6_7_32.cl
    • Inverse:
      • examples/ches2022/ntruhps2048509/pqm4/__asm_intt_32.cl
      • examples/ches2022/ntruhps2048509/pqm4/__asm_final_map.cl
• Saber
  • AVX2
    • Normal: examples/ches2022/saber/avx2/test_sabermul_nttmul_poly_ntt.cl
    • Inverse: examples/ches2022/saber/avx2/test_sabermul_nttmul_poly_invntt_tomont.cl
  • Cortex-M4
    • Normal: examples/ches2022/saber/pqm4/asm_negacyclic_ntt_32.cl
    • Inverse: examples/ches2022/saber/pqm4/asm_negacyclic_intt_32.cl

Details of the above specifications are available in Section 3.2 and
Section 4 of the paper.
To know more about CryptoLine tool and language, please read
README.CryptoLine.md.

Experiment: Figure 5

To run the experiment of verifying AVX2 Kyber NTT with various number
of cuts, run the script ches2022_run_experiments_figure5.sh in the
project root.

$ ./ches2022_run_experiments_figure5.sh

This experiment takes 24 CPU cores and the running time on our server
is around 3 hours.
The CryptoLine specifications of AVX2 Kyber NTT with various number of
cuts can be found in examples/ches2022/kyber768-avx2-cuts.
Each specification is named PQCLEAN_KYBER768_AVX2_polyvec_ntt_XX_cuts.cl
where XX denotes the number of cuts.

Experimental Results

All the log files of the experiments are stored in results-* in the
project root.
For example, log files of ches2022_run_experiments_table3.sh are
stored in results-table3 while log files of
ches2022_run_experiments_figure5.sh are stored in results-figure5.
During the verification of a specification spec.cl, the following
log files are produced.

• spec.log: verbose output such as the running time of each step
• spec_debug.log: debugging output such as the inputs for Boolector
• spec_summary.log: running time summarized in four categories,
  namely algebra, overflow, range, and total, as shown in Table 3 of
  the paper

Each of the four categories in spec_summary.log summarizes the
running time of one or more steps in spec.log.

• Algebra
  • Verifying algebraic assertions
  • Verifying algebraic specification
• Overflow
  • Verifying program safety
• Range
  • Verifying range assertions
  • Verifying range specification
• Total
  • Verification result

Extra Experiment: Lite

Besides the experiments reproducing Table 3 and Figure 5, this
artifact provides an additional lite experiment, which verifies three
NTT implementations from Table 3 using 2 CPU cores:

• Kyber768 AVX2 normal
• Kyber768 Cortex-M4 normal
• Saber AVX2 normal

Execute the following command to run this lite experiment:

$ ./ches2022_run_experiments_table3_lite.sh

Most modern personal computer can run this lite experiment.
On a MacBook Air (M1, 2020), the running time of this experiment is 1
hour.

Source Code Organization

cryptoline
  +-- LICENSE: license file
  +-- README.md: readme file
  +-- cv.ml: the main entrance of CryptoLine
  +-- cv_cli.ml: CLI mode of CryptoLine, used with the -cli argument
  +-- dune-project: dune metadata of this project
  +-- dune: components to be built by dune
  +-- ast/: abstract syntax of CryptoLine
  +-- doc/: description of CryptoLine language and a tutorial
  +-- examples/: specifications in CryptoLine languages
  +-- main/: command line arguments of CryptoLine
  +-- misc/: miscellaneous supporting files
  +-- nbits/: OCaml code extracted from [coq-nbits](https://github.com/fmlab-iis/coq-nbits)
  +-- options/: options of CryptoLine
  +-- parsers/: parsers of CryptoLine specifications
  +-- qfbv:/ translation to SMT QF_BV queries
  +-- scripts:/ some useful scripts
  +-- sim/: simulator of CryptoLine programs
  +-- typecheck/: well-formednees checker of CryptoLine specifications
  +-- utils/: utility functions
  +-- verify/: verification procedures

Each of our improvements made for verifying NTT implementations
spreads across different files.
Syntax of asserts, assumes, ghost variables, and cuts is in
ast/cryptoline.ml:instr.
Conversion from algebraic predicates in asserts, assumes, and ghost
variables to polynomials is in verify/common.ml:bv2z_instr.
Conversion from range predicates in asserts, assumes, and ghost
variables to SMT QF_BV expressions is in
verify/common.ml:bexp_instr.
Cutting specifications and processing prove with hints are in
ast/cryptoline.ml:cut_espec and ast/cryptoline.ml:cut_rspec.