From b2b1089aa67aed554a70a402bc6152d6a9c3d1de Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Tue, 10 Jun 2025 14:16:31 +0200 Subject: [PATCH 01/12] Add Readme Signed-off-by: Jonas Schneider-Bensch --- README.md | 121 +++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 119 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index ec54e2e..c65c1da 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,123 @@ [//]: # (SPDX-License-Identifier: CC-BY-4.0) [//]: # (TODO Customize project readme) -# template-code +# mlkem-rust-libcrux +`mlkem-rust-libcrux` is a portable Rust implementation of ML-KEM which +optionally supports optimizations for AVX2 and NEON platforms. -Template for creating code repositories, with basic file setup included +It originates in the `libcrux` library of formally verified +cryptographic algorithm in Rust. + +## Getting Started +To use this implementation of ML-KEM in your Rust project, run + +``` +cargo add libcrux-ml-kem +``` +in your project directory, or add + +``` +libcrux-ml-kem = "0.0.2" +``` +to your `Cargo.toml`. + + +## Status +The modules +- `mlkem512` +- `mlkem768` +- `mlkem1024` +implement the three parameter sets for ML-KEM defined in FIPS 203. + +Each module provides the following API: +- `generate_key_pair`: to generate an ML-KEM key pair, +- `encapsulate`: to encapsulate a shared secret towards a given ML-KEM public key, +- `decapsulate`: to decapsulate a shared secret from a ciphertext using an ML-KEM private key, +- `validate_public_key`: to perform validation of public keys as required by FIPS 203 prior to encapsulation, +- `validate_private_key`: to perform validation of private keys and ciphertexts as required by FIPS 203 prior to decapsulation. + +For detailed documentation, please refer to +[docs.rs](https://docs.rs/libcrux-ml-kem/latest/libcrux_ml_kem/). + +### Portable and Optimized Implementations +The crate provides portable, as well as AVX2- and NEON-optimized +implementations of the above API. By defautl, the crate's `build.rs` +will include the portable implementation and one of the optimized +implementations in the build, according to the value of +`CARGO_CFG_TARGET_ARCH`. + +In addition, the above functions perform CPU feature detection at +runtime to ensure the most efficient implementation for the given +platform is selected. + +It is recommended to rely on the automatic feature detection, but specific +builds can be forced by setting environment variables, +`LIBCRUX_ENABLE_SIMD128=1` or `LIBCRUX_ENABLE_SIMD256=1`. + +### Unpacked APIs +The default KEM API described above operates on serialized keys, +i.e. `encapsulate` will take a serialized ML-KEM public key as input +and `decapsulate` will take a serialized ML-KEM private key as input, +and these must be validated before use with `validate_public_key` +and `validate_private_key` for FIPS 203 compliance. + +In addition, in each parameter set module, (e.g. `mlkem768`) the crate +provides an API for working with "unpacked" keys, which have already +been deserialized. For some applications it may thus be advantageous +to validate key material once, then deserialized into unpacked +representation once, and to use the the already validated and +deserialized form from then on. + +The unpacked APIs are platform dependent, so they can be found in +submodules `mlkem768::portable::unpacked`, `mlkem768::avx2::unpacked`, +`mlkem768::neon::unpacked`, depending on which of these platform +specific modules are part of the build in question. + +### Common APIs +The implementation of common APIs across PQCP implementations is +work-in-progress. Progress for this implementation is tracked in issue +[`cryspen/libcrux#894`](https://github.com/cryspen/libcrux/issues/894). + +### Crate Features +The crate provides the following features. + +Default features: +- `mlkem512`, `mlkem768` & `mlkem1024`: These can be used to select + individual parameter sets. By default, all parameter sets are + included. +- `rand`: Whereas the default APIs for `generate_key_pair` and + `encapsulate` expect external provision of random bytes, this + feature enables randomized versions of these APIs (in submodules + `mlkem512::rand`, `mlkem768::rand`, `mlkem1024::rand`) which take an + `&mut impl rand_core::CryptoRng` argument to generate the required + randomness internally. +- `default-no-std` & `std`: Disabling default feature `std` provides + `no_std` support. For convenience `default-no-std` collects all default + features except `std`. + +Additional features: +- `kyber`: Provides access to an, as yet, unverified implementation of + Kyber as submitted in Round 3 of the NIST PQ competition. The Kyber + APIs follow the general structure of the ML-KEM APIs. +- `check-secret-independence`: Enforce secret independence at the + level of the Rust type-system (TODO: Elaborate why this is not + default.) +- `simd128`, `simd256`: These features force a compilation for NEON or + AVX2 targets, respectively, as discussed above. +- `incremental`: An experimental API, which allows for incremental + encapsulation. + +## Security +TODO + +## Verification Status +The code in this crate is formally verified for panic freedom, +correctness and secret independence in F* using the hax toolchain. + +TODO + +## Performance +TODO + +## FAQ +TODO From db9d6a431a823229809f2f1eaca920cd4ff5659e Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Thu, 12 Jun 2025 09:41:00 +0200 Subject: [PATCH 02/12] Elaborate on `check-secret-independence` Signed-off-by: Jonas Schneider-Bensch --- README.md | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index c65c1da..547b3b5 100644 --- a/README.md +++ b/README.md @@ -99,9 +99,14 @@ Additional features: - `kyber`: Provides access to an, as yet, unverified implementation of Kyber as submitted in Round 3 of the NIST PQ competition. The Kyber APIs follow the general structure of the ML-KEM APIs. -- `check-secret-independence`: Enforce secret independence at the - level of the Rust type-system (TODO: Elaborate why this is not - default.) +- `check-secret-independence`: All operations on ring elements in the + portable implementation use the integer types of the + `libcrux-secrets` crate under the hood. That crate allows checking a + program operating on these types for secret indepence at compile + time. Enabling the `check-secret-independence` feature switches on + this compile-time checking of secret independence. By default, the + integer types of `libcrux-secrets` transparently fall back on Rust's + standard integer types. - `simd128`, `simd256`: These features force a compilation for NEON or AVX2 targets, respectively, as discussed above. - `incremental`: An experimental API, which allows for incremental From c8fbc8b1c67cb65a70c031621508ccc22fc3a586 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Mon, 30 Jun 2025 13:32:43 +0200 Subject: [PATCH 03/12] Elaborate in 'Security' section Signed-off-by: Jonas Schneider-Bensch --- README.md | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 547b3b5..51b0dd0 100644 --- a/README.md +++ b/README.md @@ -113,7 +113,14 @@ Additional features: encapsulation. ## Security -TODO +As outlined in the description of the `check-secret-independence` +feature above, we leverage the Rust type system to ensure that secret +values are not used in operations that are known to be +non-constant time. While the implementation of constant time +operations is best-effort, as there are no guarantees from the +compiler, we follow established constant-time patterns and validate +constant-time code via inspection of the generated assembly +instructions. ## Verification Status The code in this crate is formally verified for panic freedom, From 9ce5987945575501ac43ce7dac9bbd1a6fc8d8fc Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Mon, 30 Jun 2025 13:42:06 +0200 Subject: [PATCH 04/12] Elaborate on 'Benchmark' section Signed-off-by: Jonas Schneider-Bensch --- README.md | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 51b0dd0..3aacf70 100644 --- a/README.md +++ b/README.md @@ -129,7 +129,16 @@ correctness and secret independence in F* using the hax toolchain. TODO ## Performance -TODO +We provide a dashboard of benchmark results for the main key +generation, encapsulation and decapsulation APIs across different +platforms and operating systems at +[libcrux.cryspen.com](https://libcrux.cryspen.com). + +If you wish to run the benchmarks yourself, you can do so by running +``` +cargo bench +``` +from the crate root of the `libcrux-ml-kem` crate. ## FAQ TODO From adf0a99e06828fb43f898f9ff438e4f0a3b575e7 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Mon, 30 Jun 2025 13:42:34 +0200 Subject: [PATCH 05/12] Add TBD on 'FAQ' section Signed-off-by: Jonas Schneider-Bensch --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 3aacf70..ea6e09b 100644 --- a/README.md +++ b/README.md @@ -141,4 +141,4 @@ cargo bench from the crate root of the `libcrux-ml-kem` crate. ## FAQ -TODO +TBD From 2e189c18dea1d26b9f018604c5bed26684cc74f9 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Mon, 30 Jun 2025 13:48:53 +0200 Subject: [PATCH 06/12] Elaborate on 'Verification' section Signed-off-by: Jonas Schneider-Bensch --- README.md | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index ea6e09b..4c89b1a 100644 --- a/README.md +++ b/README.md @@ -123,10 +123,14 @@ constant-time code via inspection of the generated assembly instructions. ## Verification Status -The code in this crate is formally verified for panic freedom, -correctness and secret independence in F* using the hax toolchain. - -TODO +The portable and AVX2 code for field arithmetic, NTT polynomial +arithmetic, serialization, and the generic code for high-level +algorithms is formally verified using [hax](https://hax.cryspen.com) and [F*](https://fstar-lang.org). + +Please refer to [this +file](https://github.com/cryspen/libcrux/blob/f9d1802c06ffe1dec900367e12b00edb1e7f9963/libcrux-ml-kem/proofs/verification_status.md) +in the `libcrux-ml-kem` repository for details on the verification of +this crate. ## Performance We provide a dashboard of benchmark results for the main key From 29c94fe15933b1924a3f39f01ec3ecbe25a3772f Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch Date: Mon, 30 Jun 2025 13:49:55 +0200 Subject: [PATCH 07/12] Remove SPDX TODO Signed-off-by: Jonas Schneider-Bensch --- README.md | 1 - 1 file changed, 1 deletion(-) diff --git a/README.md b/README.md index 4c89b1a..b49dc97 100644 --- a/README.md +++ b/README.md @@ -1,5 +1,4 @@ [//]: # (SPDX-License-Identifier: CC-BY-4.0) -[//]: # (TODO Customize project readme) # mlkem-rust-libcrux `mlkem-rust-libcrux` is a portable Rust implementation of ML-KEM which From cdbcefbba29364d291486d912c7c6aea9fa8b7c6 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch <124457079+jschneider-bensch@users.noreply.github.com> Date: Thu, 17 Jul 2025 15:21:37 +0200 Subject: [PATCH 08/12] Update README.md Co-authored-by: Franziskus Kiefer Signed-off-by: Jonas Schneider-Bensch <124457079+jschneider-bensch@users.noreply.github.com> --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index b49dc97..604a8e8 100644 --- a/README.md +++ b/README.md @@ -16,7 +16,7 @@ cargo add libcrux-ml-kem in your project directory, or add ``` -libcrux-ml-kem = "0.0.2" +libcrux-ml-kem = "0.0.3" ``` to your `Cargo.toml`. From b3a7331b4fbae9aaf8bb449571a3511839db615a Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch <124457079+jschneider-bensch@users.noreply.github.com> Date: Thu, 17 Jul 2025 15:21:46 +0200 Subject: [PATCH 09/12] Update README.md Co-authored-by: Franziskus Kiefer Signed-off-by: Jonas Schneider-Bensch <124457079+jschneider-bensch@users.noreply.github.com> --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 604a8e8..2c7d3a5 100644 --- a/README.md +++ b/README.md @@ -101,7 +101,7 @@ Additional features: - `check-secret-independence`: All operations on ring elements in the portable implementation use the integer types of the `libcrux-secrets` crate under the hood. That crate allows checking a - program operating on these types for secret indepence at compile + program operating on these types for secret independence at compile time. Enabling the `check-secret-independence` feature switches on this compile-time checking of secret independence. By default, the integer types of `libcrux-secrets` transparently fall back on Rust's From 20dd867ad3f7ca8bfbb4de0de32513bb2437296b Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch <124457079+jschneider-bensch@users.noreply.github.com> Date: Thu, 17 Jul 2025 15:21:55 +0200 Subject: [PATCH 10/12] Update README.md Co-authored-by: Franziskus Kiefer Signed-off-by: Jonas Schneider-Bensch <124457079+jschneider-bensch@users.noreply.github.com> --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 2c7d3a5..c918c46 100644 --- a/README.md +++ b/README.md @@ -100,7 +100,7 @@ Additional features: APIs follow the general structure of the ML-KEM APIs. - `check-secret-independence`: All operations on ring elements in the portable implementation use the integer types of the - `libcrux-secrets` crate under the hood. That crate allows checking a + [`libcrux-secrets`](https://crates.io/crates/libcrux-secrets) crate under the hood. That crate allows checking a program operating on these types for secret independence at compile time. Enabling the `check-secret-independence` feature switches on this compile-time checking of secret independence. By default, the From ebf369be1d668e44f1a0ab142497e6b54915e55d Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch <124457079+jschneider-bensch@users.noreply.github.com> Date: Thu, 17 Jul 2025 15:22:08 +0200 Subject: [PATCH 11/12] Update README.md Co-authored-by: Franziskus Kiefer Signed-off-by: Jonas Schneider-Bensch <124457079+jschneider-bensch@users.noreply.github.com> --- README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index c918c46..b75b0c8 100644 --- a/README.md +++ b/README.md @@ -114,8 +114,8 @@ Additional features: ## Security As outlined in the description of the `check-secret-independence` feature above, we leverage the Rust type system to ensure that secret -values are not used in operations that are known to be -non-constant time. While the implementation of constant time +values are not used in operations that are known to have +data-dependent execution time. While the implementation of constant time operations is best-effort, as there are no guarantees from the compiler, we follow established constant-time patterns and validate constant-time code via inspection of the generated assembly From 75bda2fdaa4e3dc1832b2e1ef924ff3bd1c62c33 Mon Sep 17 00:00:00 2001 From: Jonas Schneider-Bensch <124457079+jschneider-bensch@users.noreply.github.com> Date: Thu, 17 Jul 2025 15:22:15 +0200 Subject: [PATCH 12/12] Update README.md Co-authored-by: Franziskus Kiefer Signed-off-by: Jonas Schneider-Bensch <124457079+jschneider-bensch@users.noreply.github.com> --- README.md | 2 -- 1 file changed, 2 deletions(-) diff --git a/README.md b/README.md index b75b0c8..3092b13 100644 --- a/README.md +++ b/README.md @@ -143,5 +143,3 @@ cargo bench ``` from the crate root of the `libcrux-ml-kem` crate. -## FAQ -TBD