CT: Make poly_chknorm constant flow

The reference implementation implements poly_chknorm in variables time.
It argues that while the input coefficients itself are secret in some call
sites, it is okay to leak which coefficient lead to rejection.
It, hence, does absolute value computation in constant-time and then checks
the bound using a conditional.

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 poly_chknorm to
a constant-time implementation in the hope tha the performance penalty is
acceptable.

A minor change is that the API of poly_chknorm 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.

Resolves #153

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

Author: mkannwischer

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

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