Updates

Signed-off-by: Basil Hess <[email protected]>
open-quantum-safe · Jan 10, 2025 · 1b02f9a · 1b02f9a
1 parent be43495
commit 1b02f9a
Show file tree

Hide file tree

Showing 241 changed files with 8,398 additions and 4,339 deletions.
diff --git a/docs/algorithms/kem/ml_kem.md b/docs/algorithms/kem/ml_kem.md
@@ -7,7 +7,7 @@
 - **Authors' website**: https://pq-crystals.org/kyber/ and https://csrc.nist.gov/pubs/fips/203
 - **Specification version**: ML-KEM.
 - **Primary Source**<a name="primary-source"></a>:
-  - **Source**: https://github.com/bhess/mlkem-native/commit/8f54f09f21583fc0e29103f200fd5a42ec57665d
+  - **Source**: https://github.com/bhess/mlkem-native/commit/086b45d1ba2b5d820d4c4edb3875cbb9e023e080
   - **Implementation license (SPDX-Identifier)**: CC0-1.0 or Apache-2.0
 
 

diff --git a/docs/algorithms/kem/ml_kem.yml b/docs/algorithms/kem/ml_kem.yml
@@ -17,7 +17,7 @@ website: https://pq-crystals.org/kyber/ and https://csrc.nist.gov/pubs/fips/203
 nist-round: FIPS203
 spec-version: ML-KEM
 primary-upstream:
-  source: https://github.com/bhess/mlkem-native/commit/8f54f09f21583fc0e29103f200fd5a42ec57665d
+  source: https://github.com/bhess/mlkem-native/commit/086b45d1ba2b5d820d4c4edb3875cbb9e023e080
   spdx-license-identifier: CC0-1.0 or Apache-2.0
 parameter-sets:
 - name: ML-KEM-512

diff --git a/scripts/copy_from_upstream/copy_from_upstream.yml b/scripts/copy_from_upstream/copy_from_upstream.yml
@@ -33,8 +33,8 @@ upstreams:
   -
     name: mlkem-native
     git_url: https://github.com/bhess/mlkem-native.git
-    git_branch: updates-3
-    git_commit: 8f54f09f21583fc0e29103f200fd5a42ec57665d
+    git_branch: updates-4
+    git_commit: 086b45d1ba2b5d820d4c4edb3875cbb9e023e080
     kem_meta_path: '{pretty_name_full}_META.yml'
     kem_scheme_path: '.'
   -

diff --git a/src/kem/ml_kem/CMakeLists.txt b/src/kem/ml_kem/CMakeLists.txt
diff --git a/src/kem/ml_kem/mlkem-native_ml-kem-1024_aarch64/arith_backend.h b/src/kem/ml_kem/mlkem-native_ml-kem-1024_aarch64/arith_backend.h
@@ -3,9 +3,7 @@
  * SPDX-License-Identifier: Apache-2.0
  */
 
-#ifdef MLKEM_NATIVE_ARITH_IMPL_H
-#error Only one ARITH assembly profile can be defined -- did you include multiple profiles?
-#else
+#if !defined(MLKEM_NATIVE_ARITH_IMPL_H)
 #define MLKEM_NATIVE_ARITH_IMPL_H
 
 #include "common.h"

diff --git a/src/kem/ml_kem/mlkem-native_ml-kem-1024_aarch64/cbd.c b/src/kem/ml_kem/mlkem-native_ml-kem-1024_aarch64/cbd.c
@@ -5,6 +5,16 @@
 #include "cbd.h"
 #include <stdint.h>
 
+/* Static namespacing
+ * This is to facilitate building multiple instances
+ * of mlkem-native (e.g. with varying security levels)
+ * within a single compilation unit. */
+#define load32_littleendian MLKEM_NAMESPACE(load32_littleendian)
+#define load24_littleendian MLKEM_NAMESPACE(load24_littleendian)
+#define cbd2 MLKEM_NAMESPACE(cbd2)
+#define cbd3 MLKEM_NAMESPACE(cbd3)
+/* End of static namespacing */
+
 /*************************************************
  * Name:        load32_littleendian
  *
@@ -25,6 +35,7 @@ static uint32_t load32_littleendian(const uint8_t x[4])
   return r;
 }
 
+#if MLKEM_ETA1 == 3
 /*************************************************
  * Name:        load24_littleendian
  *
@@ -36,7 +47,6 @@ static uint32_t load32_littleendian(const uint8_t x[4])
  *
  * Returns 32-bit unsigned integer loaded from x (most significant byte is zero)
  **************************************************/
-#if MLKEM_ETA1 == 3
 static uint32_t load24_littleendian(const uint8_t x[3])
 {
   uint32_t r;
@@ -45,7 +55,7 @@ static uint32_t load24_littleendian(const uint8_t x[3])
   r |= (uint32_t)x[2] << 16;
   return r;
 }
-#endif
+#endif /* MLKEM_ETA1 == 3 */
 
 /*************************************************
  * Name:        cbd2
@@ -59,21 +69,21 @@ static uint32_t load24_littleendian(const uint8_t x[3])
  **************************************************/
 static void cbd2(poly *r, const uint8_t buf[2 * MLKEM_N / 4])
 {
-  int i;
+  unsigned i;
   for (i = 0; i < MLKEM_N / 8; i++)
   __loop__(
     invariant(i >= 0 && i <= MLKEM_N / 8)
-    invariant(array_abs_bound(r->coeffs, 0, (8 * i - 1), 2)))
+    invariant(array_abs_bound(r->coeffs, 0, 8 * i, 2)))
   {
-    int j;
+    unsigned j;
     uint32_t t = load32_littleendian(buf + 4 * i);
     uint32_t d = t & 0x55555555;
     d += (t >> 1) & 0x55555555;
 
     for (j = 0; j < 8; j++)
     __loop__(
       invariant(i >= 0 && i <= MLKEM_N / 8 && j >= 0 && j <= 8)
-      invariant(array_abs_bound(r->coeffs, 0, 8 * i + j - 1, 2)))
+      invariant(array_abs_bound(r->coeffs, 0, 8 * i + j, 2)))
     {
       const int16_t a = (d >> (4 * j + 0)) & 0x3;
       const int16_t b = (d >> (4 * j + 2)) & 0x3;
@@ -82,6 +92,7 @@ static void cbd2(poly *r, const uint8_t buf[2 * MLKEM_N / 4])
   }
 }
 
+#if MLKEM_ETA1 == 3
 /*************************************************
  * Name:        cbd3
  *
@@ -93,16 +104,15 @@ static void cbd2(poly *r, const uint8_t buf[2 * MLKEM_N / 4])
  * Arguments:   - poly *r: pointer to output polynomial
  *              - const uint8_t *buf: pointer to input byte array
  **************************************************/
-#if MLKEM_ETA1 == 3
 static void cbd3(poly *r, const uint8_t buf[3 * MLKEM_N / 4])
 {
-  int i;
+  unsigned i;
   for (i = 0; i < MLKEM_N / 4; i++)
   __loop__(
     invariant(i >= 0 && i <= MLKEM_N / 4)
-    invariant(array_abs_bound(r->coeffs, 0, (4 * i - 1), 3)))
+    invariant(array_abs_bound(r->coeffs, 0, 4 * i, 3)))
   {
-    int j;
+    unsigned j;
     const uint32_t t = load24_littleendian(buf + 3 * i);
     uint32_t d = t & 0x00249249;
     d += (t >> 1) & 0x00249249;
@@ -111,16 +121,17 @@ static void cbd3(poly *r, const uint8_t buf[3 * MLKEM_N / 4])
     for (j = 0; j < 4; j++)
     __loop__(
       invariant(i >= 0 && i <= MLKEM_N / 4 && j >= 0 && j <= 4)
-      invariant(array_abs_bound(r->coeffs, 0, 4 * i + j - 1, 3)))
+      invariant(array_abs_bound(r->coeffs, 0, 4 * i + j, 3)))
     {
       const int16_t a = (d >> (6 * j + 0)) & 0x7;
       const int16_t b = (d >> (6 * j + 3)) & 0x7;
       r->coeffs[4 * i + j] = a - b;
     }
   }
 }
-#endif
+#endif /* MLKEM_ETA1 == 3 */
 
+MLKEM_NATIVE_INTERNAL_API
 void poly_cbd_eta1(poly *r, const uint8_t buf[MLKEM_ETA1 * MLKEM_N / 4])
 {
 #if MLKEM_ETA1 == 2
@@ -132,6 +143,8 @@ void poly_cbd_eta1(poly *r, const uint8_t buf[MLKEM_ETA1 * MLKEM_N / 4])
 #endif
 }
 
+#if MLKEM_K == 2 || MLKEM_K == 4
+MLKEM_NATIVE_INTERNAL_API
 void poly_cbd_eta2(poly *r, const uint8_t buf[MLKEM_ETA2 * MLKEM_N / 4])
 {
 #if MLKEM_ETA2 == 2
@@ -140,3 +153,4 @@ void poly_cbd_eta2(poly *r, const uint8_t buf[MLKEM_ETA2 * MLKEM_N / 4])
 #error "This implementation requires eta2 = 2"
 #endif
 }
+#endif /* MLKEM_K == 2 || MLKEM_K == 4 */
diff --git a/src/kem/ml_kem/mlkem-native_ml-kem-1024_aarch64/cbd.h b/src/kem/ml_kem/mlkem-native_ml-kem-1024_aarch64/cbd.h
@@ -20,14 +20,16 @@
  * Arguments:   - poly *r: pointer to output polynomial
  *              - const uint8_t *buf: pointer to input byte array
  **************************************************/
+MLKEM_NATIVE_INTERNAL_API
 void poly_cbd_eta1(poly *r, const uint8_t buf[MLKEM_ETA1 * MLKEM_N / 4])
 __contract__(
   requires(memory_no_alias(r, sizeof(poly)))
   requires(memory_no_alias(buf, MLKEM_ETA1 * MLKEM_N / 4))
   assigns(memory_slice(r, sizeof(poly)))
-  ensures(array_abs_bound(r->coeffs, 0, MLKEM_N - 1, MLKEM_ETA1))
+  ensures(array_abs_bound(r->coeffs, 0, MLKEM_N, MLKEM_ETA1))
 );
 
+#if MLKEM_K == 2 || MLKEM_K == 4
 #define poly_cbd_eta2 MLKEM_NAMESPACE(poly_cbd_eta2)
 /*************************************************
  * Name:        poly_cbd_eta1
@@ -39,12 +41,14 @@ __contract__(
  * Arguments:   - poly *r: pointer to output polynomial
  *              - const uint8_t *buf: pointer to input byte array
  **************************************************/
+MLKEM_NATIVE_INTERNAL_API
 void poly_cbd_eta2(poly *r, const uint8_t buf[MLKEM_ETA2 * MLKEM_N / 4])
 __contract__(
   requires(memory_no_alias(r, sizeof(poly)))
   requires(memory_no_alias(buf, MLKEM_ETA2 * MLKEM_N / 4))
   assigns(memory_slice(r, sizeof(poly)))
-  ensures(array_abs_bound(r->coeffs, 0, MLKEM_N - 1, MLKEM_ETA2))
+  ensures(array_abs_bound(r->coeffs, 0, MLKEM_N, MLKEM_ETA2))
 );
+#endif /* MLKEM_K == 2 || MLKEM_K == 4 */
 
 #endif
diff --git a/src/kem/ml_kem/mlkem-native_ml-kem-1024_aarch64/cbmc.h b/src/kem/ml_kem/mlkem-native_ml-kem-1024_aarch64/cbmc.h
@@ -11,19 +11,12 @@
 
 #ifndef CBMC
 
-#define STATIC_INLINE_TESTABLE static INLINE
-#define STATIC_TESTABLE static
-
 #define __contract__(x)
 #define __loop__(x)
 #define cassert(x, y)
 
 #else /* CBMC _is_ defined, therefore we're doing proof */
 
-/* expose certain procedures to CBMC proofs that are static otherwise */
-#define STATIC_TESTABLE
-#define STATIC_INLINE_TESTABLE
-
 #define __contract__(x) x
 #define __loop__(x) x
 
@@ -76,26 +69,26 @@
 
 /*
  * Quantifiers
- * Note that the range on qvar is _inclusive_ between qvar_lb .. qvar_ub
+ * Note that the range on qvar is _exclusive_ between qvar_lb .. qvar_ub
  * https://diffblue.github.io/cbmc/contracts-quantifiers.html
  */
 
 /*
  * Prevent clang-format from corrupting CBMC's special ==> operator
  */
 /* clang-format off */
-#define forall(type, qvar, qvar_lb, qvar_ub, predicate)           \
+#define forall(qvar, qvar_lb, qvar_ub, predicate)                 \
   __CPROVER_forall                                                \
   {                                                               \
-    type qvar;                                                    \
-    ((qvar_lb) <= (qvar) && (qvar) <= (qvar_ub)) ==> (predicate)  \
+    unsigned qvar;                                                \
+    ((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==> (predicate)   \
   }
 
-#define EXISTS(type, qvar, qvar_lb, qvar_ub, predicate)         \
+#define EXISTS(qvar, qvar_lb, qvar_ub, predicate)         \
   __CPROVER_exists                                              \
   {                                                             \
-    type qvar;                                                  \
-    ((qvar_lb) <= (qvar) && (qvar) <= (qvar_ub)) && (predicate) \
+    unsigned qvar;                                              \
+    ((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) && (predicate)  \
   }
 /* clang-format on */
 
@@ -107,7 +100,7 @@
  * Boolean-value predidate that asserts that "all values of array_var are in
  * range value_lb .. value_ub (inclusive)"
  * Example:
- *  array_bound(a->coeffs, 0, MLKEM_N-1, -(MLKEM_Q - 1), MLKEM_Q - 1)
+ *  array_bound(a->coeffs, 0, MLKEM_N, -(MLKEM_Q - 1), MLKEM_Q - 1)
  * expands to
  *  __CPROVER_forall { int k; (0 <= k && k <= MLKEM_N-1) ==> ( (-(MLKEM_Q -
  *  1) <= a->coeffs[k]) && (a->coeffs[k] <= (MLKEM_Q - 1))) }
@@ -120,18 +113,18 @@
 #define CBMC_CONCAT_(left, right) left##right
 #define CBMC_CONCAT(left, right) CBMC_CONCAT_(left, right)
 
-#define array_bound_core(indextype, qvar, qvar_lb, qvar_ub, array_var, \
+#define array_bound_core(qvar, qvar_lb, qvar_ub, array_var,            \
                          value_lb, value_ub)                           \
   __CPROVER_forall                                                     \
   {                                                                    \
-    indextype qvar;                                                    \
-    ((qvar_lb) <= (qvar) && (qvar) <= (qvar_ub)) ==>                   \
+    unsigned qvar;                                                     \
+    ((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==>                    \
         (((value_lb) <= (array_var[(qvar)])) &&                        \
         ((array_var[(qvar)]) <= (value_ub)))                           \
   }
 
 #define array_bound(array_var, qvar_lb, qvar_ub, value_lb, value_ub) \
-  array_bound_core(int, CBMC_CONCAT(_cbmc_idx, __LINE__), (qvar_lb), \
+  array_bound_core(CBMC_CONCAT(_cbmc_idx, __LINE__), (qvar_lb),      \
                    (qvar_ub), (array_var), (value_lb), (value_ub))
 
 

diff --git a/src/kem/ml_kem/mlkem-native_ml-kem-1024_aarch64/common.h b/src/kem/ml_kem/mlkem-native_ml-kem-1024_aarch64/common.h
@@ -7,6 +7,8 @@
 
 #if defined(MLKEM_NATIVE_CONFIG_FILE)
 #include MLKEM_NATIVE_CONFIG_FILE
+#else
+#include "config.h"
 #endif /* MLKEM_NATIVE_CONFIG_FILE */
 
 #include "params.h"
@@ -22,9 +24,21 @@
 #endif
 #endif
 
-/* This must come after the inclusion of the backend metadata
- * since the backend choice may be part of the namespace. */
-#include "namespace.h"
+#if !defined(MLKEM_NATIVE_ARITH_BACKEND_NAME)
+#define MLKEM_NATIVE_ARITH_BACKEND_NAME C
+#endif
+
+#if !defined(MLKEM_NATIVE_FIPS202_BACKEND_NAME)
+#define MLKEM_NATIVE_FIPS202_BACKEND_NAME C
+#endif
+
+/* For a monobuild (where all compilation units are merged into one), mark
+ * all non-public API as static since they don't need external linkage. */
+#if !defined(MLKEM_NATIVE_MONOBUILD)
+#define MLKEM_NATIVE_INTERNAL_API
+#else
+#define MLKEM_NATIVE_INTERNAL_API static
+#endif
 
 /* On Apple platforms, we need to emit leading underscore
  * in front of assembly symbols. We thus introducee a separate