CT: Make polyvecl_chknorm and polyveck_chknorm constant flow

The reference implementation implements polyvecl_chknorm and polyveck_chknorm
in variable time, i.e., it leaks which polynomial violated the rejection bound.

This approach appears safe, but somewhat unclean as it is still operating on
_secret data_. When performing constant-time testing it also requires a
number of declassifications.

This commit takes a more conservative approach and changes both funcitons to
constant-time implementations in the hope tha the performance penalty is
acceptable.

A minor change is that the API is changed to returning
0xFFFFFFFF in the case of failure to be able to re-use existing constant-time
primitives.
CBMC proofs are adjusted accordingly.

Signed-off-by: Matthias J. Kannwischer <[email protected]>

Author: mkannwischer

mldsa/polyvec.c

@@ -292,23 +292,26 @@ void mld_polyvecl_pointwise_acc_montgomery(mld_poly *w, const mld_polyvecl *u,
 }
 
 
-int mld_polyvecl_chknorm(const mld_polyvecl *v, int32_t bound)
+uint32_t mld_polyvecl_chknorm(const mld_polyvecl *v, int32_t bound)
 {
   unsigned int i;
+  uint32_t t = 0;
 
   for (i = 0; i < MLDSA_L; ++i)
   __loop__(
     invariant(i <= MLDSA_L)
-    invariant(forall(k1, 0, i, array_abs_bound(v->vec[k1].coeffs, 0, MLDSA_N, bound)))
+    invariant(t == 0 || t == 0xFFFFFFFF)
+    invariant((t == 0) == forall(k1, 0, i, array_abs_bound(v->vec[k1].coeffs, 0, MLDSA_N, bound)))
   )
   {
-    if (mld_poly_chknorm(&v->vec[i], bound))
-    {
-      return 1;
-    }
+    /* Reference: Leaks which polynomial violates the bound via a conditional.
+     * We are more conservative to reduce the number of declassifications in
+     * constant-time testing.
+     */
+    t |= mld_poly_chknorm(&v->vec[i], bound);
   }
 
-  return 0;
+  return t;
 }
 
 /**************************************************************/
@@ -447,23 +450,26 @@ void mld_polyveck_pointwise_poly_montgomery(mld_polyveck *r, const mld_poly *a,
 }
 
 
-int mld_polyveck_chknorm(const mld_polyveck *v, int32_t bound)
+uint32_t mld_polyveck_chknorm(const mld_polyveck *v, int32_t bound)
 {
   unsigned int i;
+  uint32_t t = 0;
 
   for (i = 0; i < MLDSA_K; ++i)
   __loop__(
     invariant(i <= MLDSA_K)
-    invariant(forall(k1, 0, i, array_abs_bound(v->vec[k1].coeffs, 0, MLDSA_N, bound)))
+    invariant(t == 0 || t == 0xFFFFFFFF)
+    invariant((t == 0) == forall(k1, 0, i, array_abs_bound(v->vec[k1].coeffs, 0, MLDSA_N, bound)))
   )
   {
-    if (mld_poly_chknorm(&v->vec[i], bound))
-    {
-      return 1;
-    }
+    /* Reference: Leaks which polynomial violates the bound via a conditional.
+     * We are more conservative to reduce the number of declassifications in
+     * constant-time testing.
+     */
+    t |= mld_poly_chknorm(&v->vec[i], bound);
   }
 
-  return 0;
+  return t;
 }
 
 void mld_polyveck_power2round(mld_polyveck *v1, mld_polyveck *v0,

mldsa/polyvec.h

@@ -195,15 +195,15 @@ __contract__(
  *              - int32_t B: norm bound
  *
  * Returns 0 if norm of all polynomials is strictly smaller than B <=
- * (MLDSA_Q-1)/8 and 1 otherwise.
+ * (MLDSA_Q-1)/8 and 0xFFFFFFFF otherwise.
  **************************************************/
-int mld_polyvecl_chknorm(const mld_polyvecl *v, int32_t B)
+uint32_t mld_polyvecl_chknorm(const mld_polyvecl *v, int32_t B)
 __contract__(
   requires(memory_no_alias(v, sizeof(mld_polyvecl)))
   requires(0 <= B && B <= (MLDSA_Q - 1) / 8)
   requires(forall(k0, 0, MLDSA_L,
     array_bound(v->vec[k0].coeffs, 0, MLDSA_N, -REDUCE32_RANGE_MAX, REDUCE32_RANGE_MAX)))
-  ensures(return_value == 0 || return_value == 1)
+  ensures(return_value == 0 || return_value == 0xFFFFFFFF)
   ensures((return_value == 0) == forall(k1, 0, MLDSA_L, array_abs_bound(v->vec[k1].coeffs, 0, MLDSA_N, B)))
 );
 
@@ -384,16 +384,16 @@ __contract__(
  *              - int32_t B: norm bound
  *
  * Returns 0 if norm of all polynomials are strictly smaller than B <=
- *(MLDSA_Q-1)/8 and 1 otherwise.
+ *(MLDSA_Q-1)/8 and 0xFFFFFFFF otherwise.
  **************************************************/
-int mld_polyveck_chknorm(const mld_polyveck *v, int32_t B)
+uint32_t mld_polyveck_chknorm(const mld_polyveck *v, int32_t B)
 __contract__(
   requires(memory_no_alias(v, sizeof(mld_polyveck)))
   requires(0 <= B && B <= (MLDSA_Q - 1) / 8)
   requires(forall(k0, 0, MLDSA_K,
                   array_bound(v->vec[k0].coeffs, 0, MLDSA_N,
                               -REDUCE32_RANGE_MAX, REDUCE32_RANGE_MAX)))
-  ensures(return_value == 0 || return_value == 1)
+  ensures(return_value == 0 || return_value == 0xFFFFFFFF)
   ensures((return_value == 0) == forall(k1, 0, MLDSA_K, array_abs_bound(v->vec[k1].coeffs, 0, MLDSA_N, B)))
 );
 

mldsa/sign.c

@@ -313,7 +313,7 @@ __contract__(
   mld_polyvecl y, z;
   mld_polyveck w2, w1, w0, h;
   mld_poly cp;
-  int z_invalid, w0_invalid, h_invalid;
+  uint32_t z_invalid, w0_invalid, h_invalid;
 
   /* Sample intermediate vector y */
   mld_polyvecl_uniform_gamma1(&y, rhoprime, nonce);

proofs/cbmc/polyveck_chknorm/polyveck_chknorm_harness.c

@@ -7,6 +7,6 @@ void harness(void)
 {
   int32_t b;
   mld_polyveck *v;
-  int r;
+  uint32_t r;
   r = mld_polyveck_chknorm(v, b);
 }