Axiomatize FIPS-202 Hash functions

This PR adds CBMC contracts to the FIPS202 hash functions and their MLKEM specific variants. We also adjust indcpa_keypair_derand() to avoid explicit aliasing of actual parameters in the call to hash_g(), as is already done in AWS-LC. Signed-off-by: Rod Chapman <[email protected]>
pq-code-package · Nov 12, 2024 · 86e3eac · 86e3eac
1 parent b5e1be1
commit 86e3eac
Show file tree

Hide file tree

Showing 4 changed files with 76 additions and 53 deletions.
diff --git a/fips202/fips202.h b/fips202/fips202.h
@@ -34,7 +34,8 @@ typedef struct {
 void shake128_absorb(shake128ctx *state, const uint8_t *input,
                      size_t inlen)  // clang-format off
 REQUIRES(IS_FRESH(state, sizeof(shake128ctx)))
-REQUIRES(IS_FRESH(input, inlen)) ASSIGNS(OBJECT_WHOLE(state));
+REQUIRES(IS_FRESH(input, inlen))
+ASSIGNS(OBJECT_UPTO(state, sizeof(shake128ctx)));
 // clang-format on
 
 /* Squeeze output out of the sponge.
@@ -45,8 +46,8 @@ REQUIRES(IS_FRESH(input, inlen)) ASSIGNS(OBJECT_WHOLE(state));
 void shake128_squeezeblocks(uint8_t *output, size_t nblocks,
                             shake128ctx *state)  // clang-format off
 REQUIRES(IS_FRESH(state, sizeof(shake128ctx)))
-REQUIRES(IS_FRESH(output, nblocks *SHAKE128_RATE))
-ASSIGNS(OBJECT_WHOLE(output), OBJECT_WHOLE(state));
+REQUIRES(IS_FRESH(output, nblocks * SHAKE128_RATE))
+ASSIGNS(OBJECT_UPTO(output, nblocks * SHAKE128_RATE), OBJECT_UPTO(state, sizeof(shake128ctx)));
 // clang-format on
 
 
@@ -76,37 +77,36 @@ void shake256_inc_squeeze(uint8_t *output, size_t outlen,
 #define shake256_inc_ctx_release FIPS202_NAMESPACE(shake256_inc_ctx_release)
 void shake256_inc_ctx_release(shake256incctx *state);
 
-/* One-stop SHAKE256 call */
+/* One-stop SHAKE256 call. Aliasing between input and
+ * output is not permitted */
 #define shake256 FIPS202_NAMESPACE(shake256)
 void shake256(uint8_t *output, size_t outlen, const uint8_t *input,
               size_t inlen)  // clang-format off
-// Refine +prove this spec, e.g. add disjointness constraints?
-REQUIRES(READABLE(input, inlen))
-REQUIRES(WRITEABLE(output, outlen))
+REQUIRES(IS_FRESH(input, inlen))
+REQUIRES(IS_FRESH(output, outlen))
 ASSIGNS(OBJECT_UPTO(output, outlen));
 // clang-format on
 
-/* One-stop SHA3-256 shop */
+/* One-stop SHA3_256 call. Aliasing between input and
+ * output is not permitted */
+#define SHA3_256_HASHBYTES 32
 #define sha3_256 FIPS202_NAMESPACE(sha3_256)
 void sha3_256(uint8_t *output, const uint8_t *input,
               size_t inlen)  // clang-format off
 REQUIRES(IS_FRESH(input, inlen))
-REQUIRES(IS_FRESH(output, 32))
-ASSIGNS(OBJECT_WHOLE(output));
+REQUIRES(IS_FRESH(output, SHA3_256_HASHBYTES))
+ASSIGNS(OBJECT_UPTO(output, SHA3_256_HASHBYTES));
 // clang-format on
 
-/* One-stop SHA3-512 shop */
+/* One-stop SHA3_512 call. Aliasing between input and
+ * output is not permitted */
+#define SHA3_512_HASHBYTES 64
 #define sha3_512 FIPS202_NAMESPACE(sha3_512)
 void sha3_512(uint8_t *output, const uint8_t *input,
               size_t inlen)  // clang-format off
-REQUIRES(
-    /* Case A: Aliasing between input and output */
-    (output == input && inlen <= 64 && IS_FRESH(output, 64))
- ||
-    /* Case B: Disjoint input and output */
-    (IS_FRESH(input, inlen) && IS_FRESH(output, 64))
-)
-ASSIGNS(OBJECT_WHOLE(output));
+REQUIRES(IS_FRESH(input, inlen))
+REQUIRES(IS_FRESH(output, SHA3_512_HASHBYTES))
+ASSIGNS(OBJECT_UPTO(output, SHA3_512_HASHBYTES));
 // clang-format on
 
 #endif
diff --git a/mlkem/indcpa.c b/mlkem/indcpa.c
@@ -419,10 +419,12 @@ void indcpa_keypair_derand(uint8_t pk[MLKEM_INDCPA_PUBLICKEYBYTES],
   polyvec a[MLKEM_K], e, pkpv, skpv;
   polyvec_mulcache skpv_cache;
 
-  // Add MLKEM_K for domain separation of security levels
-  memcpy(buf, coins, MLKEM_SYMBYTES);
-  buf[MLKEM_SYMBYTES] = MLKEM_K;
-  hash_g(buf, buf, MLKEM_SYMBYTES + 1);
+  uint8_t coins_with_domain_separator[MLKEM_SYMBYTES + 1];
+  // Concatenate coins with MLKEM_K for domain separation of security levels
+  memcpy(coins_with_domain_separator, coins, MLKEM_SYMBYTES);
+  coins_with_domain_separator[MLKEM_SYMBYTES] = MLKEM_K;
+
+  hash_g(buf, coins_with_domain_separator, MLKEM_SYMBYTES + 1);
 
   gen_matrix(a, publicseed, 0 /* no transpose */);
 

diff --git a/mlkem/symmetric-shake.c b/mlkem/symmetric-shake.c
@@ -6,18 +6,6 @@
 #include "params.h"
 #include "symmetric.h"
 
-/*************************************************
- * Name:        mlkem_shake256_prf
- *
- * Description: Usage of SHAKE256 as a PRF, concatenates secret and public input
- *              and then generates outlen bytes of SHAKE256 output
- *
- * Arguments:   - uint8_t *out: pointer to output
- *              - size_t outlen: number of requested output bytes
- *              - const uint8_t *key: pointer to the key (of length
- *MLKEM_SYMBYTES)
- *              - uint8_t nonce: single-byte nonce (public PRF input)
- **************************************************/
 void mlkem_shake256_prf(uint8_t *out, size_t outlen,
                         const uint8_t key[MLKEM_SYMBYTES], uint8_t nonce) {
   uint8_t extkey[MLKEM_SYMBYTES + 1];
@@ -28,18 +16,6 @@ void mlkem_shake256_prf(uint8_t *out, size_t outlen,
   shake256(out, outlen, extkey, sizeof(extkey));
 }
 
-/*************************************************
- * Name:        mlkem_shake256_rkprf
- *
- * Description: Usage of SHAKE256 as a PRF, concatenates secret and public input
- *              and then generates outlen bytes of SHAKE256 output
- *
- * Arguments:   - uint8_t *out: pointer to output
- *              - size_t outlen: number of requested output bytes
- *              - const uint8_t *key: pointer to the key (of length
- *MLKEM_SYMBYTES)
- *              - uint8_t nonce: single-byte nonce (public PRF input)
- **************************************************/
 void mlkem_shake256_rkprf(uint8_t out[MLKEM_SSBYTES],
                           const uint8_t key[MLKEM_SYMBYTES],
                           const uint8_t input[MLKEM_CIPHERTEXTBYTES]) {

diff --git a/mlkem/symmetric.h b/mlkem/symmetric.h
@@ -11,21 +11,66 @@
 #include "cbmc.h"
 
 #define mlkem_shake256_prf MLKEM_NAMESPACE(mlkem_shake256_prf)
+/*************************************************
+ * Name:        mlkem_shake256_prf
+ *
+ * Ref:         FIPS-203 Section 4.1. Function PRF (eq 4.3)
+ *
+ * Description: Usage of SHAKE256 as a PRF, concatenates secret and public input
+ *              and then generates outlen bytes of SHAKE256 output
+ *
+ * Arguments:   - uint8_t *out: pointer to output
+ *              - size_t outlen: number of requested output bytes
+ *              - const uint8_t *key: pointer to the key (of length
+ *                MLKEM_SYMBYTES)
+ *              - uint8_t nonce: single-byte nonce (public PRF input)
+ *
+ *              out and key may NOT be aliased.
+ **************************************************/
 void mlkem_shake256_prf(uint8_t *out, size_t outlen,
-                        const uint8_t key[MLKEM_SYMBYTES], uint8_t nonce);
+                        const uint8_t key[MLKEM_SYMBYTES],
+                        uint8_t nonce)  // clang-format off
+REQUIRES(IS_FRESH(out, outlen))
+REQUIRES(IS_FRESH(key, MLKEM_SYMBYTES))
+ASSIGNS(OBJECT_UPTO(out, outlen));
+// clang-format on
 
 #define mlkem_shake256_rkprf MLKEM_NAMESPACE(mlkem_shake256_rkprf)
+/*************************************************
+ * Name:        mlkem_shake256_rkprf
+ *
+ * Ref:         FIPS-203 Section 4.1. Hash function J
+ *
+ * Description: Usage of SHAKE256 as a PRF, concatenates key with input
+ *              and then generates MLKEM_SSBYTES bytes of SHAKE256 output
+ *
+ * Arguments:   - uint8_t *out: pointer to output
+ *              - const uint8_t *key: pointer to the key (of length
+ *                MLKEM_SYMBYTES)
+ *              - const uint8_t *input: pointer to the input (of length
+ *                MLKEM_CIPHERTEXTBYTES)
+ *
+ *              out, key, and input may NOT be aliased.
+ **************************************************/
 void mlkem_shake256_rkprf(
     uint8_t out[MLKEM_SSBYTES], const uint8_t key[MLKEM_SYMBYTES],
     const uint8_t input[MLKEM_CIPHERTEXTBYTES])  // clang-format off
-// TODO: Refine + prove this spec, e.g. add disjointness constraints?
-REQUIRES(READABLE(input, MLKEM_CIPHERTEXTBYTES))
-REQUIRES(READABLE(key, MLKEM_SYMBYTES))
-REQUIRES(WRITEABLE(out, MLKEM_SSBYTES))
-ASSIGNS(OBJECT_UPTO(out, MLKEM_SSBYTES));  // clang-format on
+REQUIRES(IS_FRESH(out, MLKEM_SSBYTES))
+REQUIRES(IS_FRESH(key, MLKEM_SYMBYTES))
+REQUIRES(IS_FRESH(input, MLKEM_CIPHERTEXTBYTES))
+ASSIGNS(OBJECT_UPTO(out, MLKEM_SSBYTES));
+// clang-format on
 
+
+// Macros denoting FIPS-203 specific Hash functions
+
+// Hash function H, FIPS-201 4.1 (eq 4.4)
 #define hash_h(OUT, IN, INBYTES) sha3_256(OUT, IN, INBYTES)
+
+// Hash function G, FIPS-201 4.1 (eq 4.5)
 #define hash_g(OUT, IN, INBYTES) sha3_512(OUT, IN, INBYTES)
+
+// Macros denoting FIPS-203 specific PRFs
 #define prf(OUT, OUTBYTES, KEY, NONCE) \
   mlkem_shake256_prf(OUT, OUTBYTES, KEY, NONCE)
 #define rkprf(OUT, KEY, INPUT) mlkem_shake256_rkprf(OUT, KEY, INPUT)