Add option for destruction of intermediate values

FIPS-203, Section 3.3 demands the destruction of intermediate
values before returning to the caller. This commit adds a compile-time
option MLK_DESTRUCT_INTERMEDIATES which implements that.

When set, MLK_DESTRUCT_INTERMEDIATES causes all intermediate stack buffers
to be wiped prior to function return, via a new function ct_zeroize()
in verify.h. (NB: The constant-time'ness is not relevant here, but
conceptually the function is still best-placed in verify.h alongside
other functions which, when naively implemented, would be prone to
harmful compiler optimization -- ct_zeroize fits this category).

By default, ct_zeroize() is implemented via SecureZeroMemory on
Windows, and a plain memset + compiler barrier otherwise. Using
memset_s would be preferred, but there is no portable way of
detecting whether it is available. If users need to register a
custom ct_zeroize, they can do so by defining MLK_CT_ZEROIZE_NATIVE
and defining ct_zeroize_native, similar to how the arithmetic and
FIPS-202 backends work.

Even if MLK_DESTRUCT_INTERMEDIATES is not set, there are still dummy
function calls to ct_zeroize() in the code. Those are no-ops, but
are kept nonetheless to force the CBMC proofs to consider them, based
on a contract for ct_zeroize().

Signed-off-by: Hanno Becker <[email protected]>

examples/monolithic_build/mlkem_native_monobuild.c

@@ -88,6 +88,7 @@
 #undef MLK_ARITH_BACKEND_FILE
 #undef MLK_CONFIG_H
 #undef MLK_DEFAULT_NAMESPACE_PREFIX
+#undef MLK_DESTRUCT_INTERMEDIATES
 #undef MLK_FIPS202_BACKEND_FILE
 #undef MLK_NAMESPACE_PREFIX
 /* mlkem/indcpa.h */
@@ -283,13 +284,15 @@
 #undef MLK_ALIGN
 #undef MLK_ALWAYS_INLINE
 #undef MLK_DEFAULT_ALIGN
+#undef MLK_HAVE_INLINE_ASM
 #undef MLK_INLINE
 #undef MLK_RESTRICT
 #undef MLK_SYS_AARCH64
 #undef MLK_SYS_AARCH64_EB
 #undef MLK_SYS_BIG_ENDIAN
 #undef MLK_SYS_H
 #undef MLK_SYS_LITTLE_ENDIAN
+#undef MLK_SYS_WINDOWS
 #undef MLK_SYS_X86_64
 #undef MLK_SYS_X86_64_AVX2
 /* mlkem/verify.h */
@@ -303,6 +306,7 @@
 #undef ct_opt_blocker_u64
 #undef ct_sel_int16
 #undef ct_sel_uint8
+#undef ct_zeroize
 #undef value_barrier_i32
 #undef value_barrier_u32
 #undef value_barrier_u8

mlkem/config.h

@@ -235,6 +235,41 @@
  *****************************************************************************/
 /* #define MLK_FIPS202X4_CUSTOM_HEADER "SOME_FILE.h" */
 
+/******************************************************************************
+ * Name:        MLK_DESTRUCT_INTERMEDIATES
+ *
+ * Description: If this option is set, functions are instrumented to zeroize
+ *              intermediate stack buffers prior to returning.
+ *
+ *              WARNING:
+ *              This feature reduces the likelihood of secrets leaking
+ *              on the stack, but does not eliminate it!
+ *              The C standard makes no guarantee about where a compiler
+ *              allocates structures and whether/where it makes copies of
+ *              them. Also, in addition to entire structures, there may also
+ *              be potentially exploitable leakage of individual values on the
+ *stack.
+ *
+ *              If you need bullet-proof zeroization of the stack, you need to
+ *              consider additional measures atop of what this feature provides.
+ *
+ *              The default implementation uses SecureZeroMemory on Windows
+ *              and a memset + compiler barrier otherwise. If you want to
+ *replace this default implementation, set MLK_USE_CT_ZEROIZE_NATIVE and provide
+ *a definition for `ct_zeroize_native(void *ptr, size_t len);`.
+ *
+ *****************************************************************************/
+#define MLK_DESTRUCT_INTERMEDIATES
+/* #define MLK_USE_CT_ZEROIZE_NATIVE
+   #if !defined(__ASSEMBLER__)
+   #include "sys.h"
+   static MLK_INLINE void ct_zeroize_native(void *ptr, size_t len)
+   {
+       ... your implementation ...
+   }
+   #endif
+*/
+
 /*************************  Config internals  ********************************/
 
 /* Default namespace

mlkem/indcpa.c

@@ -247,6 +247,13 @@ void gen_matrix(polyvec *a, const uint8_t seed[MLKEM_SYMBYTES], int transposed)
       poly_permute_bitrev_to_custom(a[i].vec[j].coeffs);
     }
   }
+
+  /* FIPS 203. Section 3.3 Destruction of intermediate values.
+   * This is a no-op unless MLK_DESTRUCT_INTERMEDIATES is set. */
+  ct_zeroize(seed0, sizeof(seed0));
+  ct_zeroize(seed1, sizeof(seed1));
+  ct_zeroize(seed2, sizeof(seed2));
+  ct_zeroize(seed3, sizeof(seed3));
 }
 
 /*************************************************
@@ -350,6 +357,15 @@ void indcpa_keypair_derand(uint8_t pk[MLKEM_INDCPA_PUBLICKEYBYTES],
 
   pack_sk(sk, &skpv);
   pack_pk(pk, &pkpv, publicseed);
+
+  /* FIPS 203. Section 3.3 Destruction of intermediate values.
+   * This is a no-op unless MLK_DESTRUCT_INTERMEDIATES is set. */
+  ct_zeroize(buf, sizeof(buf));
+  ct_zeroize(coins_with_domain_separator, sizeof(coins_with_domain_separator));
+  ct_zeroize(a, sizeof(a));
+  ct_zeroize(&e, sizeof(e));
+  ct_zeroize(&skpv, sizeof(skpv));
+  ct_zeroize(&skpv_cache, sizeof(skpv_cache));
 }
 
 
@@ -419,6 +435,18 @@ void indcpa_enc(uint8_t c[MLKEM_INDCPA_BYTES],
   poly_reduce(&v);
 
   pack_ciphertext(c, &b, &v);
+
+  /* FIPS 203. Section 3.3 Destruction of intermediate values.
+   * This is a no-op unless MLK_DESTRUCT_INTERMEDIATES is set. */
+  ct_zeroize(seed, sizeof(seed));
+  ct_zeroize(&sp, sizeof(sp));
+  ct_zeroize(&sp_cache, sizeof(sp_cache));
+  ct_zeroize(&b, sizeof(b));
+  ct_zeroize(&v, sizeof(v));
+  ct_zeroize(at, sizeof(at));
+  ct_zeroize(&k, sizeof(k));
+  ct_zeroize(&ep, sizeof(ep));
+  ct_zeroize(&epp, sizeof(epp));
 }
 
 MLK_INTERNAL_API
@@ -442,6 +470,12 @@ void indcpa_dec(uint8_t m[MLKEM_INDCPA_MSGBYTES],
   poly_reduce(&v);
 
   poly_tomsg(m, &v);
+
+  /* FIPS 203. Section 3.3 Destruction of intermediate values.
+   * This is a no-op unless MLK_DESTRUCT_INTERMEDIATES is set. */
+  ct_zeroize(&skpv, sizeof(skpv));
+  ct_zeroize(&v, sizeof(v));
+  ct_zeroize(&sb, sizeof(sb));
 }
 
 /* To facilitate single-compilation-unit (SCU) builds, undefine all macros.

mlkem/kem.c

@@ -121,6 +121,11 @@ int crypto_kem_keypair(uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES],
   MLK_ALIGN uint8_t coins[2 * MLKEM_SYMBYTES];
   randombytes(coins, 2 * MLKEM_SYMBYTES);
   crypto_kem_keypair_derand(pk, sk, coins);
+
+  /* FIPS 203. Section 3.3 Destruction of intermediate values.
+   * This is a no-op unless MLK_DESTRUCT_INTERMEDIATES is set. */
+  ct_zeroize(coins, sizeof(coins));
+
   return 0;
 }
 
@@ -148,16 +153,31 @@ int crypto_kem_enc_derand(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES],
   indcpa_enc(ct, buf, pk, kr + MLKEM_SYMBYTES);
 
   memcpy(ss, kr, MLKEM_SYMBYTES);
+
+  /* FIPS 203. Section 3.3 Destruction of intermediate values. */
+  /* This is only in effect if MLK_DESTRUCT_INTERMEDIATES is set; otherwise,
+   * ct_zeroize() is a no-op. We keep the calls nonetheless to ensure that the
+   * CBMC proofs incorporate them (based on the contract for ct_zeroize). */
+  ct_zeroize(buf, sizeof(buf));
+  ct_zeroize(kr, sizeof(kr));
+
   return 0;
 }
 
 int crypto_kem_enc(uint8_t ct[MLKEM_INDCCA_CIPHERTEXTBYTES],
                    uint8_t ss[MLKEM_SSBYTES],
                    const uint8_t pk[MLKEM_INDCCA_PUBLICKEYBYTES])
 {
+  int res;
   MLK_ALIGN uint8_t coins[MLKEM_SYMBYTES];
   randombytes(coins, MLKEM_SYMBYTES);
-  return crypto_kem_enc_derand(ct, ss, pk, coins);
+  res = crypto_kem_enc_derand(ct, ss, pk, coins);
+
+  /* FIPS 203. Section 3.3 Destruction of intermediate values.
+   * This is a no-op unless MLK_DESTRUCT_INTERMEDIATES is set. */
+  ct_zeroize(coins, sizeof(coins));
+
+  return res;
 }
 
 int crypto_kem_dec(uint8_t ss[MLKEM_SSBYTES],
@@ -168,6 +188,8 @@ int crypto_kem_dec(uint8_t ss[MLKEM_SSBYTES],
   MLK_ALIGN uint8_t buf[2 * MLKEM_SYMBYTES];
   /* Will contain key, coins */
   MLK_ALIGN uint8_t kr[2 * MLKEM_SYMBYTES];
+  MLK_ALIGN uint8_t tmp[MLKEM_SYMBYTES + MLKEM_INDCCA_CIPHERTEXTBYTES];
+
   const uint8_t *pk = sk + MLKEM_INDCPA_SECRETKEYBYTES;
 
   if (check_sk(sk))
@@ -183,27 +205,25 @@ int crypto_kem_dec(uint8_t ss[MLKEM_SSBYTES],
   hash_g(kr, buf, 2 * MLKEM_SYMBYTES);
 
   /* Recompute and compare ciphertext */
-  {
-    /* Temporary buffer */
-    MLK_ALIGN uint8_t cmp[MLKEM_INDCCA_CIPHERTEXTBYTES];
-    /* coins are in kr+MLKEM_SYMBYTES */
-    indcpa_enc(cmp, buf, pk, kr + MLKEM_SYMBYTES);
-    fail = ct_memcmp(ct, cmp, MLKEM_INDCCA_CIPHERTEXTBYTES);
-  }
+  /* coins are in kr+MLKEM_SYMBYTES */
+  indcpa_enc(tmp, buf, pk, kr + MLKEM_SYMBYTES);
+  fail = ct_memcmp(ct, tmp, MLKEM_INDCCA_CIPHERTEXTBYTES);
 
   /* Compute rejection key */
-  {
-    /* Temporary buffer */
-    MLK_ALIGN uint8_t tmp[MLKEM_SYMBYTES + MLKEM_INDCCA_CIPHERTEXTBYTES];
-    memcpy(tmp, sk + MLKEM_INDCCA_SECRETKEYBYTES - MLKEM_SYMBYTES,
-           MLKEM_SYMBYTES);
-    memcpy(tmp + MLKEM_SYMBYTES, ct, MLKEM_INDCCA_CIPHERTEXTBYTES);
-    hash_j(ss, tmp, sizeof(tmp));
-  }
+  memcpy(tmp, sk + MLKEM_INDCCA_SECRETKEYBYTES - MLKEM_SYMBYTES,
+         MLKEM_SYMBYTES);
+  memcpy(tmp + MLKEM_SYMBYTES, ct, MLKEM_INDCCA_CIPHERTEXTBYTES);
+  hash_j(ss, tmp, sizeof(tmp));
 
   /* Copy true key to return buffer if fail is 0 */
   ct_cmov_zero(ss, kr, MLKEM_SYMBYTES, fail);
 
+  /* FIPS 203. Section 3.3 Destruction of intermediate values.
+   * This is a no-op unless MLK_DESTRUCT_INTERMEDIATES is set. */
+  ct_zeroize(buf, sizeof(buf));
+  ct_zeroize(kr, sizeof(kr));
+  ct_zeroize(tmp, sizeof(tmp));
+
   return 0;
 }
 

mlkem/poly_k.c

@@ -255,6 +255,17 @@ void poly_getnoise_eta1_4x(poly *r0, poly *r1, poly *r2, poly *r3,
   debug_assert_abs_bound(r1, MLKEM_N, MLKEM_ETA1 + 1);
   debug_assert_abs_bound(r2, MLKEM_N, MLKEM_ETA1 + 1);
   debug_assert_abs_bound(r3, MLKEM_N, MLKEM_ETA1 + 1);
+
+  /* FIPS 203. Section 3.3 Destruction of intermediate values.
+   * This is a no-op unless MLK_DESTRUCT_INTERMEDIATES is set. */
+  ct_zeroize(buf0, sizeof(buf0));
+  ct_zeroize(buf1, sizeof(buf1));
+  ct_zeroize(buf2, sizeof(buf2));
+  ct_zeroize(buf3, sizeof(buf3));
+  ct_zeroize(extkey0, sizeof(extkey0));
+  ct_zeroize(extkey1, sizeof(extkey1));
+  ct_zeroize(extkey2, sizeof(extkey2));
+  ct_zeroize(extkey3, sizeof(extkey3));
 }
 
 #if MLKEM_K == 2 || MLKEM_K == 4
@@ -297,6 +308,11 @@ void poly_getnoise_eta2(poly *r, const uint8_t seed[MLKEM_SYMBYTES],
   poly_cbd_eta2(r, buf);
 
   debug_assert_abs_bound(r, MLKEM_N, MLKEM_ETA1 + 1);
+
+  /* FIPS 203. Section 3.3 Destruction of intermediate values.
+   * This is a no-op unless MLK_DESTRUCT_INTERMEDIATES is set. */
+  ct_zeroize(buf, sizeof(buf));
+  ct_zeroize(extkey, sizeof(extkey));
 }
 #endif /* MLKEM_K == 2 || MLKEM_K == 4 */
 
@@ -352,6 +368,17 @@ void poly_getnoise_eta1122_4x(poly *r0, poly *r1, poly *r2, poly *r3,
   debug_assert_abs_bound(r1, MLKEM_N, MLKEM_ETA1 + 1);
   debug_assert_abs_bound(r2, MLKEM_N, MLKEM_ETA2 + 1);
   debug_assert_abs_bound(r3, MLKEM_N, MLKEM_ETA2 + 1);
+
+  /* FIPS 203. Section 3.3 Destruction of intermediate values.
+   * This is a no-op unless MLK_DESTRUCT_INTERMEDIATES is set. */
+  ct_zeroize(buf0, sizeof(buf0));
+  ct_zeroize(buf1, sizeof(buf1));
+  ct_zeroize(buf2, sizeof(buf2));
+  ct_zeroize(buf3, sizeof(buf3));
+  ct_zeroize(extkey0, sizeof(extkey0));
+  ct_zeroize(extkey1, sizeof(extkey1));
+  ct_zeroize(extkey2, sizeof(extkey2));
+  ct_zeroize(extkey3, sizeof(extkey3));
 }
 #endif /* MLKEM_K == 2 */
 

mlkem/sampling.c

@@ -188,6 +188,13 @@ void poly_rej_uniform_x4(poly *vec, uint8_t *seed[4])
   }
 
   xof_x4_release(&statex);
+
+  /* FIPS 203. Section 3.3 Destruction of intermediate values.
+   * This is a no-op unless MLK_DESTRUCT_INTERMEDIATES is set. */
+  ct_zeroize(buf0, sizeof(buf0));
+  ct_zeroize(buf1, sizeof(buf1));
+  ct_zeroize(buf2, sizeof(buf2));
+  ct_zeroize(buf3, sizeof(buf3));
 }
 
 MLK_INTERNAL_API

mlkem/sys.h

@@ -23,6 +23,14 @@
 #endif
 #endif /* __x86_64__ */
 
+#if defined(_WIN32)
+#define MLK_SYS_WINDOWS
+#endif /* _WIN32 */
+
+#if !defined(MLK_NO_ASM) && (defined(__GNUC__) || defined(__clang__))
+#define MLK_HAVE_INLINE_ASM
+#endif
+
 /* Try to find endianness, if not forced through CFLAGS already */
 #if !defined(MLK_SYS_LITTLE_ENDIAN) && !defined(MLK_SYS_BIG_ENDIAN)
 #if defined(__BYTE_ORDER__)

mlkem/verify.h

@@ -25,6 +25,7 @@
 #define ct_sel_int16 MLK_NAMESPACE(ct_sel_int16)
 #define ct_memcmp MLK_NAMESPACE(ct_memcmp)
 #define ct_cmov_zero MLK_NAMESPACE(ct_cmov_zero)
+#define ct_zeroize MLK_NAMESPACE(ct_zeroize)
 /* End of static namespacing */
 
 /* Constant-time comparisons and conditional operations
@@ -59,8 +60,7 @@
 
 */
 
-#if (defined(__GNUC__) || defined(__clang__)) && !defined(CBMC) && \
-    !defined(MLKEM_NO_ASM_VALUE_BARRIER)
+#if defined(MLK_HAVE_INLINE_ASM) && !defined(MLKEM_NO_ASM_VALUE_BARRIER)
 #define MLK_USE_ASM_VALUE_BARRIER
 #endif
 
@@ -314,4 +314,47 @@ __contract__(
   }
 }
 
+/*************************************************
+ * Name:        ct_zeroize
+ *
+ * Description: Force-zeroize a buffer.
+ *
+ * Arguments:   uint8_t *r:       pointer to byte array to be zeroed
+ *              size_t len:       Amount of bytes to be zeroed
+ **************************************************/
+static MLK_INLINE void ct_zeroize(void *r, size_t len)
+__contract__(
+  requires(memory_no_alias(r, len))
+  assigns(memory_slice(r, len))
+);
+
+#if defined(MLK_DESTRUCT_INTERMEDIATES)
+static MLK_INLINE void ct_zeroize(void *ptr, size_t len)
+{
+#if defined(MLK_USE_CT_ZEROIZE_NATIVE)
+  ct_zeroize_native(ptr, len);
+#elif defined(MLK_SYS_WINDOWS)
+#include <memory.h>
+  SecureZeroMemory(ptr, len);
+#elif defined(MLK_HAVE_INLINE_ASM)
+#include <string.h>
+  memset(ptr, 0, len);
+  /* This follows OpenSSL and seems sufficient to prevent the compiler
+   * from optimizing away the memset.
+   *
+   * If there was a reliable way to detect availablility of memset_s(),
+   * that would be preferred. */
+  __asm__ __volatile__("" : : "r"(ptr) : "memory");
+#else
+#error MLK_ZEROIZE_STACK set but no default implementation available.
+#endif
+}
+#else  /* MLK_DESTRUCT_INTERMEDIATES */
+static MLK_INLINE void ct_zeroize(void *ptr, size_t len)
+{
+  ((void)ptr);
+  ((void)len);
+}
+#endif /* MLK_ZEROIZE_SECRET_STACK */
+
 #endif /* MLK_VERIFY_H */

proofs/cbmc/crypto_kem_dec/Makefile

@@ -19,7 +19,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/kem.c
 
 CHECK_FUNCTION_CONTRACTS=$(MLK_NAMESPACE)dec
-USE_FUNCTION_CONTRACTS=$(MLK_NAMESPACE)sha3_512 $(MLK_NAMESPACE)sha3_256 $(MLK_NAMESPACE)indcpa_enc $(MLK_NAMESPACE)indcpa_dec $(MLK_NAMESPACE)shake256 $(MLK_NAMESPACE)ct_memcmp $(MLK_NAMESPACE)ct_cmov_zero memcmp
+USE_FUNCTION_CONTRACTS=$(MLK_NAMESPACE)sha3_512 $(MLK_NAMESPACE)sha3_256 $(MLK_NAMESPACE)indcpa_enc $(MLK_NAMESPACE)indcpa_dec $(MLK_NAMESPACE)shake256 $(MLK_NAMESPACE)ct_memcmp $(MLK_NAMESPACE)ct_cmov_zero memcmp $(MLK_NAMESPACE)ct_zeroize
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 

proofs/cbmc/crypto_kem_enc/Makefile

@@ -19,7 +19,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mlkem/kem.c
 
 CHECK_FUNCTION_CONTRACTS=$(MLK_NAMESPACE)enc
-USE_FUNCTION_CONTRACTS=$(MLK_NAMESPACE)enc_derand randombytes
+USE_FUNCTION_CONTRACTS=$(MLK_NAMESPACE)enc_derand randombytes $(MLK_NAMESPACE)ct_zeroize
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1