ML-KEM libjade

Current status

This repository includes two ML-KEM-768 Jasmin implementations, src/mlkem768_amd64_avx2/ and src/mlkem768_amd64_ref/:

• they will be updated soon, as significant performance and security improvements are on the verge of completion.
• they were also published in the artifact of the CRYPTO 24 paper, Formally verifying Kyber Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt.

TLDR: How can I quickly test this code?

0. Clone this repository.
1. Go to examples/mlkem768_amd64_avx2 (or examples/mlkem768_amd64_ref) and run make, then ./example.
2. Read file example.c, including the discussion in comments.
3. Check the corresponding src/ folders.

If you are already familiar with ML-KEM-768 API, this should be enough for you to prototype something.

---

We provide more details next. When running make, you should be able to see the following:

cc -Wall -Wextra  -o example -I ../../src/mlkem768_amd64_avx2/ example.c ../../src/mlkem768_amd64_avx2/mlkem768_amd64_avx2.s -lcrypto

Which produces a program named example that runs the corresponding Jasmin ML-KEM-768 implementation and prints the inputs/outputs of the executed functions to the terminal. Note that ./example is not deterministic, meaning that running more than once always prints different data because the program gets random bytes for each execution. There are some important comments in example.c, regarding random bytes that the reader must not skip: just for illustrative purposes, we use the function RAND_bytes from OpenSSL, and that is why -lcrypto is used during compilation. More details below.

Next, we provide an overview of some files: first, those located in the src/ folder, and then those in the examples/ folder. In the folder src/mlkem768_amd64_avx2/ you can find the following (the contents are similar for src/mlkem768_amd64_ref/):

• mlkem768_amd64_avx2.jazz is the Jasmin implementation, which is available in a single file for simplicity.

• mlkem768_amd64_avx2.s is the assembly file resulting from compiling mlkem768_amd64_avx2.jazz with the Jasmin compiler, release 2024.07.2. This file defines the ML-KEM-768 functions that can be used in C/C++/etc. You can recompile this file if you wish; you will need a recent release of the Jasmin compiler in such a case. We provide the assembly file so the user can get started quickly.

• api.h is the C header file for using mlkem768_amd64_avx2.s. It contains the function's prototypes and corresponding macros defining, for instance, the public and secret key lengths.

• jasmin_syscall.h is the file that provides the prototype for __jasmin_syscall_randombytes__. The ML-KEM-768 implementation needs to get cryptographically secure random bytes. In the case of the randomized implementation, the implementation itself needs to call an external function to obtain these random bytes. It is the user's responsibility to provide such a function to the Jasmin implementation, in this case, __jasmin_syscall_randombytes__.

In folder examples/mlkem768_amd64_avx2 (respectively, examples/mlkem768_amd64_ref), you can find the following two files:

• Makefile defines a rule to build the program example and to remove it, with make clean.

• example.c includes discussions about random bytes, the API, and namespacing, as well as the code that calls the functions for key generation, encapsulation, and decapsulation, followed by a check to ensure that the shared secret from encapsulate is equal to the one from decapsulate. It contains examples of randomized and derandomized APIs.