Merge pull request #1227 from pq-code-package/no_std_header

hanno-becker · web-flow · commit 82d321525ef2 · 2025-10-11T11:51:57.000+01:00
Remove single occurrence of memcmp
diff --git a/dev/aarch64_clean/src/arith_native_aarch64.h b/dev/aarch64_clean/src/arith_native_aarch64.h
@@ -6,6 +6,7 @@
 #define MLK_DEV_AARCH64_CLEAN_SRC_ARITH_NATIVE_AARCH64_H
 
 #include <stdint.h>
+
 #include "../../../cbmc.h"
 #include "../../../common.h"
 
diff --git a/dev/fips202/aarch64/src/fips202_native_aarch64.h b/dev/fips202/aarch64/src/fips202_native_aarch64.h
@@ -6,6 +6,7 @@
 #define MLK_DEV_FIPS202_AARCH64_SRC_FIPS202_NATIVE_AARCH64_H
 
 #include <stdint.h>
+
 #include "../../../../cbmc.h"
 #include "../../../../common.h"
 
diff --git a/dev/fips202/aarch64/src/keccakf1600_round_constants.c b/dev/fips202/aarch64/src/keccakf1600_round_constants.c
@@ -13,6 +13,7 @@
     !defined(MLK_CONFIG_MULTILEVEL_NO_SHARED)
 
 #include <stdint.h>
+
 #include "fips202_native_aarch64.h"
 
 MLK_ALIGN const uint64_t mlk_keccakf1600_round_constants[] = {
diff --git a/dev/x86_64/meta.h b/dev/x86_64/meta.h
@@ -30,7 +30,6 @@
 #define MLK_USE_NATIVE_POLY_DECOMPRESS_D11
 
 #if !defined(__ASSEMBLER__)
-#include <string.h>
 #include "../../common.h"
 #include "../api.h"
 #include "src/arith_native_x86_64.h"
diff --git a/dev/x86_64/src/compress_avx2.c b/dev/x86_64/src/compress_avx2.c
@@ -24,7 +24,6 @@
 
 #include <immintrin.h>
 #include <stdint.h>
-#include <string.h>
 #include "arith_native_x86_64.h"
 #include "consts.h"
 
diff --git a/mlkem/src/compress.c b/mlkem/src/compress.c
@@ -21,7 +21,7 @@
 #if !defined(MLK_CONFIG_MULTILEVEL_NO_SHARED)
 
 #include <stdint.h>
-#include <string.h>
+
 #include "cbmc.h"
 #include "compress.h"
 #include "debug.h"
diff --git a/mlkem/src/compress.h b/mlkem/src/compress.h
@@ -20,8 +20,8 @@
 #ifndef MLK_COMPRESS_H
 #define MLK_COMPRESS_H
 
-#include <stddef.h>
 #include <stdint.h>
+
 #include "cbmc.h"
 #include "common.h"
 #include "debug.h"
diff --git a/mlkem/src/fips202/fips202.c b/mlkem/src/fips202/fips202.c
@@ -34,9 +34,8 @@
 #include "../common.h"
 #if !defined(MLK_CONFIG_MULTILEVEL_NO_SHARED)
 
-#include <stddef.h>
 #include <stdint.h>
-#include <string.h>
+
 #include "../verify.h"
 #include "fips202.h"
 #include "keccakf1600.h"
diff --git a/mlkem/src/fips202/fips202.h b/mlkem/src/fips202/fips202.h
@@ -4,8 +4,8 @@
  */
 #ifndef MLK_FIPS202_FIPS202_H
 #define MLK_FIPS202_FIPS202_H
-#include <stddef.h>
 #include <stdint.h>
+
 #include "../cbmc.h"
 #include "../common.h"
 
diff --git a/mlkem/src/fips202/fips202x4.c b/mlkem/src/fips202/fips202x4.c
@@ -15,7 +15,6 @@
 #include "../common.h"
 #if !defined(MLK_CONFIG_MULTILEVEL_NO_SHARED)
 
-#include <string.h>
 #include "../verify.h"
 #include "fips202.h"
 #include "fips202x4.h"
diff --git a/mlkem/src/fips202/fips202x4.h b/mlkem/src/fips202/fips202x4.h
@@ -5,7 +5,6 @@
 #ifndef MLK_FIPS202_FIPS202X4_H
 #define MLK_FIPS202_FIPS202X4_H
 
-#include <stddef.h>
 #include <stdint.h>
 
 #include "../cbmc.h"
diff --git a/mlkem/src/fips202/keccakf1600.c b/mlkem/src/fips202/keccakf1600.c
@@ -26,7 +26,6 @@
  * implementation @[supercop, crypto_hash/keccakc512/simple/]
  * by Ronny Van Keer, and the public domain @[tweetfips] implementation. */
 
-#include <assert.h>
 #include <stdint.h>
 
 #include "keccakf1600.h"
diff --git a/mlkem/src/fips202/native/aarch64/src/fips202_native_aarch64.h b/mlkem/src/fips202/native/aarch64/src/fips202_native_aarch64.h
@@ -6,6 +6,7 @@
 #define MLK_FIPS202_NATIVE_AARCH64_SRC_FIPS202_NATIVE_AARCH64_H
 
 #include <stdint.h>
+
 #include "../../../../cbmc.h"
 #include "../../../../common.h"
 
diff --git a/mlkem/src/fips202/native/aarch64/src/keccakf1600_round_constants.c b/mlkem/src/fips202/native/aarch64/src/keccakf1600_round_constants.c
@@ -13,6 +13,7 @@
     !defined(MLK_CONFIG_MULTILEVEL_NO_SHARED)
 
 #include <stdint.h>
+
 #include "fips202_native_aarch64.h"
 
 MLK_ALIGN const uint64_t mlk_keccakf1600_round_constants[] = {
diff --git a/mlkem/src/indcpa.c b/mlkem/src/indcpa.c
@@ -17,9 +17,7 @@
  *   https://github.com/pq-crystals/kyber/tree/main/ref
  */
 
-#include <stddef.h>
 #include <stdint.h>
-#include <string.h>
 
 #include "cbmc.h"
 #include "debug.h"
diff --git a/mlkem/src/kem.c b/mlkem/src/kem.c
@@ -22,9 +22,7 @@
  *   https://github.com/pq-crystals/kyber/tree/main/ref
  */
 
-#include <stddef.h>
 #include <stdint.h>
-#include <string.h>
 
 #include "indcpa.h"
 #include "kem.h"
@@ -39,16 +37,6 @@
 #define mlk_check_pct MLK_ADD_PARAM_SET(mlk_check_pct)
 /* End of parameter set namespacing */
 
-#if defined(CBMC)
-/* Redeclaration with contract needed for CBMC only */
-int memcmp(const void *str1, const void *str2, size_t n)
-__contract__(
-  requires(memory_no_alias(str1, n))
-  requires(memory_no_alias(str2, n))
-);
-#endif /* CBMC */
-
-
 /* Reference: Not implemented in the reference implementation @[REF]. */
 MLK_EXTERNAL_API
 MLK_MUST_CHECK_RETURN_VALUE
@@ -95,8 +83,11 @@ int crypto_kem_check_sk(const uint8_t sk[MLKEM_INDCCA_SECRETKEYBYTES])
 
   mlk_hash_h(test, sk + MLKEM_INDCPA_SECRETKEYBYTES,
              MLKEM_INDCCA_PUBLICKEYBYTES);
-  res = memcmp(sk + MLKEM_INDCCA_SECRETKEYBYTES - 2 * MLKEM_SYMBYTES, test,
-               MLKEM_SYMBYTES)
+  /* This doesn't have to be a constant-time memcmp, but it's the only place
+   * in the library where a normal memcmp would be used otherwise, so for sake
+   * of minimizing stdlib dependency, we use our constant-time one anyway. */
+  res = mlk_ct_memcmp(sk + MLKEM_INDCCA_SECRETKEYBYTES - 2 * MLKEM_SYMBYTES,
+                      test, MLKEM_SYMBYTES)
             ? -1
             : 0;
 
diff --git a/mlkem/src/native/x86_64/meta.h b/mlkem/src/native/x86_64/meta.h
@@ -30,7 +30,6 @@
 #define MLK_USE_NATIVE_POLY_DECOMPRESS_D11
 
 #if !defined(__ASSEMBLER__)
-#include <string.h>
 #include "../../common.h"
 #include "../api.h"
 #include "src/arith_native_x86_64.h"
diff --git a/mlkem/src/native/x86_64/src/compress_avx2.c b/mlkem/src/native/x86_64/src/compress_avx2.c
@@ -24,7 +24,6 @@
 
 #include <immintrin.h>
 #include <stdint.h>
-#include <string.h>
 #include "arith_native_x86_64.h"
 #include "consts.h"
 
diff --git a/mlkem/src/poly.c b/mlkem/src/poly.c
@@ -21,7 +21,7 @@
 #if !defined(MLK_CONFIG_MULTILEVEL_NO_SHARED)
 
 #include <stdint.h>
-#include <string.h>
+
 #include "cbmc.h"
 #include "debug.h"
 #include "poly.h"
diff --git a/mlkem/src/poly.h b/mlkem/src/poly.h
@@ -15,8 +15,8 @@
 #ifndef MLK_POLY_H
 #define MLK_POLY_H
 
-#include <stddef.h>
 #include <stdint.h>
+
 #include "cbmc.h"
 #include "common.h"
 #include "debug.h"
diff --git a/mlkem/src/poly_k.c b/mlkem/src/poly_k.c
@@ -23,7 +23,6 @@
  */
 
 #include <stdint.h>
-#include <string.h>
 
 #include "compress.h"
 #include "debug.h"
diff --git a/mlkem/src/randombytes.h b/mlkem/src/randombytes.h
@@ -5,7 +5,6 @@
 #ifndef MLK_RANDOMBYTES_H
 #define MLK_RANDOMBYTES_H
 
-#include <stddef.h>
 #include <stdint.h>
 
 #include "cbmc.h"
diff --git a/mlkem/src/symmetric.h b/mlkem/src/symmetric.h
@@ -15,8 +15,8 @@
 #ifndef MLK_SYMMETRIC_H
 #define MLK_SYMMETRIC_H
 
-#include <stddef.h>
 #include <stdint.h>
+
 #include "cbmc.h"
 #include "common.h"
 #include MLK_FIPS202_HEADER_FILE
diff --git a/mlkem/src/verify.h b/mlkem/src/verify.h
@@ -30,9 +30,8 @@
 #ifndef MLK_VERIFY_H
 #define MLK_VERIFY_H
 
-#include <limits.h>
-#include <stddef.h>
 #include <stdint.h>
+
 #include "cbmc.h"
 #include "common.h"
 
@@ -319,7 +318,8 @@ __contract__(ensures(return_value == (cond ? a : b)))
  * Arguments:   const uint8_t *a: pointer to first byte array
  *              const uint8_t *b: pointer to second byte array
  *              size_t len:       length of the byte arrays, upper-bounded
- *                                to INT_MAX to control proof complexity
+ *                                to UINT16_MAX to control proof complexity
+ *                                only.
  *
  * Returns 0 if the byte arrays are equal, a non-zero value otherwise
  *
@@ -339,7 +339,7 @@ __contract__(ensures(return_value == (cond ? a : b)))
 static MLK_INLINE uint8_t mlk_ct_memcmp(const uint8_t *a, const uint8_t *b,
                                         const size_t len)
 __contract__(
-  requires(len <= INT_MAX)
+  requires(len <= UINT16_MAX)
   requires(memory_no_alias(a, len))
   requires(memory_no_alias(b, len))
   ensures((return_value == 0) == forall(i, 0, len, (a[i] == b[i]))))
diff --git a/proofs/cbmc/crypto_kem_check_sk/Makefile b/proofs/cbmc/crypto_kem_check_sk/Makefile
@@ -20,7 +20,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/src/kem.c
 
 CHECK_FUNCTION_CONTRACTS=mlk_check_sk
-USE_FUNCTION_CONTRACTS=mlk_sha3_256 mlk_zeroize memcmp
+USE_FUNCTION_CONTRACTS=mlk_sha3_256 mlk_zeroize mlk_ct_memcmp
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 
