Merge pull request #392 from pq-code-package/constant-time-2

CT: Make poly_chknorm constant flow

Author: hanno-becker

mldsa/ct.h

@@ -176,7 +176,9 @@ __contract__(
  **************************************************/
 /* TODO: proof */
 static MLD_INLINE uint32_t mld_ct_cmask_neg_i32(int32_t x)
-__contract__(ensures(return_value == ((x < 0) ? 0xFFFFFFFF : 0)))
+__contract__(
+  ensures(return_value == ((x < 0) ? 0xFFFFFFFF : 0))
+)
 {
   int64_t tmp = mld_value_barrier_i64((int64_t)x);
   tmp >>= 31;
@@ -197,7 +199,7 @@ __contract__(ensures(return_value == ((x < 0) ? 0xFFFFFFFF : 0)))
  *
  **************************************************/
 /* TODO: proof */
-static MLD_INLINE uint32_t mld_ct_abs_i32(int32_t x)
+static MLD_INLINE int32_t mld_ct_abs_i32(int32_t x)
 __contract__(
   requires(x >= -INT32_MAX)
   ensures(return_value == ((x < 0) ? -x : x))

mldsa/poly.c

@@ -234,35 +234,35 @@ void mld_poly_use_hint(mld_poly *b, const mld_poly *a, const mld_poly *h)
 /* Reference: explicitly checks the bound B to be <= (MLDSA_Q - 1) / 8).
  * This is unnecessary as it's always a compile-time constant.
  * We instead model it as a precondition.
+ * Checking the bound is performed using a conditional arguing
+ * that it is okay to leak which coefficient violates the bound (while the
+ * coefficient itself must remain secret).
+ * We instead perform everything in constant-time.
  */
-int mld_poly_chknorm(const mld_poly *a, int32_t B)
+uint32_t mld_poly_chknorm(const mld_poly *a, int32_t B)
 {
   unsigned int i;
-  int rc = 0;
-  int32_t t;
+  uint32_t t = 0;
   mld_assert_bound(a->coeffs, MLDSA_N, -REDUCE32_RANGE_MAX, REDUCE32_RANGE_MAX);
 
-  /* It is ok to leak which coefficient violates the bound since
-     the probability for each coefficient is independent of secret
-     data but we must not leak the sign of the centralized representative. */
 
   for (i = 0; i < MLDSA_N; ++i)
   __loop__(
     invariant(i <= MLDSA_N)
-    invariant(rc == 0 || rc == 1)
-    invariant((rc == 0) == array_abs_bound(a->coeffs, 0, i, B))
+    invariant(t == 0 || t == 0xFFFFFFFF)
+    invariant((t == 0) == array_abs_bound(a->coeffs, 0, i, B))
   )
   {
-    /* Absolute value */
-    t = mld_ct_abs_i32(a->coeffs[i]);
+    /* Reference: Leaks which coefficient violates the bound via a conditional.
+     * We are more conservative to reduce the number of declassifications in
+     * constant-time testing.
+     */
 
-    if (t >= B)
-    {
-      rc = 1;
-    }
+    /* if (abs(a[i]) >= B) */
+    t |= mld_ct_cmask_neg_i32(B - 1 - mld_ct_abs_i32(a->coeffs[i]));
   }
 
-  return rc;
+  return t;
 }
 
 /*************************************************

mldsa/poly.h

@@ -295,15 +295,15 @@ __contract__(
  * Arguments:   - const mld_poly *a: pointer to polynomial
  *              - int32_t B: norm bound
  *
- * Returns 0 if norm is strictly smaller than B <= (MLDSA_Q-1)/8 and 1
- *otherwise.
+ * Returns 0 if norm is strictly smaller than B <= (MLDSA_Q-1)/8 and 0xFFFFFFFF
+ * otherwise.
  **************************************************/
-int mld_poly_chknorm(const mld_poly *a, int32_t B)
+uint32_t mld_poly_chknorm(const mld_poly *a, int32_t B)
 __contract__(
   requires(memory_no_alias(a, sizeof(mld_poly)))
   requires(0 <= B && B <= (MLDSA_Q - 1) / 8)
   requires(array_bound(a->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) == array_abs_bound(a->coeffs, 0, MLDSA_N, B))
 );
 

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/poly_chknorm/Makefile

@@ -20,7 +20,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
 PROJECT_SOURCES += $(SRCDIR)/mldsa/poly.c
 
 CHECK_FUNCTION_CONTRACTS=$(MLD_NAMESPACE)poly_chknorm
-USE_FUNCTION_CONTRACTS=mld_ct_abs_i32
+USE_FUNCTION_CONTRACTS=mld_ct_abs_i32 mld_ct_cmask_neg_i32
 APPLY_LOOP_CONTRACTS=on
 USE_DYNAMIC_FRAMES=1
 

proofs/cbmc/poly_chknorm/poly_chknorm_harness.c

@@ -7,7 +7,7 @@
 void harness(void)
 {
   mld_poly *a;
-  int r;
+  uint32_t r;
   int32_t B;
   r = mld_poly_chknorm(a, B);
 }

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);
 }