Skip to content

Commit

Permalink
Debug/CBMC: Interpret debug-assertions as proof obligations
Browse files Browse the repository at this point in the history 
Previously, runtime assertions via debug_assert_xxx and CBMC
assertions via cassert(...) were separate.

This commit modifies the implementation of the debug assertion
macros so that when CBMC is used, debug assertions are intepreted
as proof obligations.

This removes some redundancy and non-uniformity in the code,
and also reduces the likelihood that debug assertions and CBMC
contracts get out of sync. In some case, this actually happened,
and the commit fixes this. The commit also adds further bounds
assertions in alignment with pre/post conditions.

A slight nuisance is that the debug assertions cannot flatten
nested structures like polyvec for the bounds check, running
into issue diffblue/cbmc#8570. We
work around this by introducing a new `xxx_2d` (for 2-dimensional)
macro which takes two dimensions and uses a two-step array
access, circumventing the above CBMC issue.

Signed-off-by: Hanno Becker <[email protected]>
  • Loading branch information
@hanno-becker
hanno-becker committed Jan 17, 2025
1 parent ab9d84d commit 79757a2
Show file tree
Hide file tree
Showing 12 changed files with 161 additions and 49 deletions.
45 changes: 45 additions & 0 deletions examples/monolithic_build/mlkem_native_monobuild.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -373,6 +373,11 @@
#undef debug_assert
#endif

/* mlkem/debug/debug.h */
#if defined(debug_assert)
#undef debug_assert
#endif

/* mlkem/debug/debug.h */
#if defined(debug_assert_abs_bound)
#undef debug_assert_abs_bound
Expand All @@ -383,6 +388,31 @@
#undef debug_assert_abs_bound
#endif

/* mlkem/debug/debug.h */
#if defined(debug_assert_abs_bound)
#undef debug_assert_abs_bound
#endif

/* mlkem/debug/debug.h */
#if defined(debug_assert_abs_bound_2d)
#undef debug_assert_abs_bound_2d
#endif

/* mlkem/debug/debug.h */
#if defined(debug_assert_abs_bound_2d)
#undef debug_assert_abs_bound_2d
#endif

/* mlkem/debug/debug.h */
#if defined(debug_assert_abs_bound_2d)
#undef debug_assert_abs_bound_2d
#endif

/* mlkem/debug/debug.h */
#if defined(debug_assert_bound)
#undef debug_assert_bound
#endif

/* mlkem/debug/debug.h */
#if defined(debug_assert_bound)
#undef debug_assert_bound
Expand All @@ -393,6 +423,21 @@
#undef debug_assert_bound
#endif

/* mlkem/debug/debug.h */
#if defined(debug_assert_bound_2d)
#undef debug_assert_bound_2d
#endif

/* mlkem/debug/debug.h */
#if defined(debug_assert_bound_2d)
#undef debug_assert_bound_2d
#endif

/* mlkem/debug/debug.h */
#if defined(debug_assert_bound_2d)
#undef debug_assert_bound_2d
#endif

/* mlkem/debug/debug.h */
#if defined(mlkem_debug_assert)
#undef mlkem_debug_assert
Expand Down
6 changes: 3 additions & 3 deletions mlkem/cbmc.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -119,13 +119,13 @@
{ \
unsigned qvar; \
((qvar_lb) <= (qvar) && (qvar) < (qvar_ub)) ==> \
(((int)(value_lb) <= (array_var[(qvar)])) && \
((array_var[(qvar)]) < (int)(value_ub))) \
(((int)(value_lb) <= ((array_var)[(qvar)])) && \
(((array_var)[(qvar)]) < (int)(value_ub))) \
}

#define array_bound(array_var, qvar_lb, qvar_ub, value_lb, value_ub) \
array_bound_core(CBMC_CONCAT(_cbmc_idx, __LINE__), (qvar_lb), \
(qvar_ub), (array_var), (value_lb), (value_ub))
(qvar_ub), (array_var), (value_lb), (value_ub))
/* clang-format on */

/* Wrapper around array_bound operating on absolute values.
Expand Down
58 changes: 47 additions & 11 deletions mlkem/debug/debug.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -50,24 +50,17 @@ void mlkem_debug_check_bounds(const char *file, int line, const int16_t *ptr,
*
* val: Value that's asserted to be non-zero
*/
#define debug_assert(val) \
do \
{ \
mlkem_debug_assert(__FILE__, __LINE__, (val)); \
} while (0)
#define debug_assert(val) mlkem_debug_assert(__FILE__, __LINE__, (val))

/* Check bounds in array of int16_t's
* ptr: Base of int16_t array; will be explicitly cast to int16_t*,
* so you may pass a byte-compatible type such as poly or polyvec.
* len: Number of int16_t in array
* value_lb: Inclusive lower value bound
* value_ub: Exclusive upper value bound */
#define debug_assert_bound(ptr, len, value_lb, value_ub) \
do \
{ \
mlkem_debug_check_bounds(__FILE__, __LINE__, (const int16_t *)(ptr), \
(len), (value_lb)-1, (value_ub)); \
} while (0)
#define debug_assert_bound(ptr, len, value_lb, value_ub) \
mlkem_debug_check_bounds(__FILE__, __LINE__, (const int16_t *)(ptr), (len), \
(value_lb)-1, (value_ub))

/* Check absolute bounds in array of int16_t's
* ptr: Base of array, expression of type int16_t*
Expand All @@ -76,6 +69,38 @@ void mlkem_debug_check_bounds(const char *file, int line, const int16_t *ptr,
#define debug_assert_abs_bound(ptr, len, value_abs_bd) \
debug_assert_bound((ptr), (len), (-(value_abs_bd) + 1), (value_abs_bd))

/* Version of bounds assertions for 2-dimensional arrays */
#define debug_assert_bound_2d(ptr, len0, len1, value_lb, value_ub) \
debug_assert_bound((ptr), ((len0) * (len1)), (value_lb), (value_ub))

#define debug_assert_abs_bound_2d(ptr, len0, len1, value_abs_bd) \
debug_assert_abs_bound((ptr), ((len0) * (len1)), (value_abs_bd))

/* When running CBMC, convert debug assertions into proof obligations */
#elif defined(CBMC)

#include "../cbmc.h"

#define debug_assert(val) cassert(val)

#define debug_assert_bound(ptr, len, value_lb, value_ub) \
cassert(array_bound(((int16_t *)(ptr)), 0, (len), (value_lb), (value_ub)))

#define debug_assert_abs_bound(ptr, len, value_abs_bd) \
cassert(array_abs_bound(((int16_t *)(ptr)), 0, (len), (value_abs_bd)))

/* Because of https://github.com/diffblue/cbmc/issues/8570, we can't
* just use a single flattened array_bound(...) here. */
#define debug_assert_bound_2d(ptr, M, N, value_lb, value_ub) \
cassert(forall(kN, 0, (M), \
array_bound(&((int16_t(*)[(N)])(ptr))[kN][0], 0, (N), \
(value_lb), (value_ub))))

#define debug_assert_abs_bound_2d(ptr, M, N, value_abs_bd) \
cassert(forall(kN, 0, (M), \
array_abs_bound(&((int16_t(*)[(N)])(ptr))[kN][0], 0, (N), \
(value_abs_bd))))

#else /* MLKEM_DEBUG */

#define debug_assert(val) \
Expand All @@ -91,6 +116,17 @@ void mlkem_debug_check_bounds(const char *file, int line, const int16_t *ptr,
{ \
} while (0)

#define debug_assert_bound_2d(ptr, len0, len1, value_lb, value_ub) \
do \
{ \
} while (0)

#define debug_assert_abs_bound_2d(ptr, len0, len1, value_abs_bd) \
do \
{ \
} while (0)


#endif /* MLKEM_DEBUG */

#endif /* MLKEM_DEBUG_H */
6 changes: 3 additions & 3 deletions mlkem/indcpa.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,7 @@
static void pack_pk(uint8_t r[MLKEM_INDCPA_PUBLICKEYBYTES], polyvec *pk,
const uint8_t seed[MLKEM_SYMBYTES])
{
debug_assert_abs_bound(pk, MLKEM_K * MLKEM_N, MLKEM_Q);
debug_assert_bound_2d(pk, MLKEM_K, MLKEM_N, 0, MLKEM_Q);
polyvec_tobytes(r, pk);
memcpy(r + MLKEM_POLYVECBYTES, seed, MLKEM_SYMBYTES);
}
Expand Down Expand Up @@ -91,7 +91,7 @@ static void unpack_pk(polyvec *pk, uint8_t seed[MLKEM_SYMBYTES],
**************************************************/
static void pack_sk(uint8_t r[MLKEM_INDCPA_SECRETKEYBYTES], polyvec *sk)
{
debug_assert_abs_bound(sk, MLKEM_K * MLKEM_N, MLKEM_Q);
debug_assert_bound_2d(sk, MLKEM_K, MLKEM_N, 0, MLKEM_Q);
polyvec_tobytes(r, sk);
}

Expand Down Expand Up @@ -353,7 +353,7 @@ void gen_matrix(polyvec *a, const uint8_t seed[MLKEM_SYMBYTES], int transposed)
i++;
}

cassert(i == MLKEM_K * MLKEM_K);
debug_assert(i == MLKEM_K * MLKEM_K);

/*
* The public matrix is generated in NTT domain. If the native backend
Expand Down
18 changes: 15 additions & 3 deletions mlkem/poly.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,8 @@ MLKEM_NATIVE_INTERNAL_API
void poly_compress_du(uint8_t r[MLKEM_POLYCOMPRESSEDBYTES_DU], const poly *a)
{
unsigned j;
debug_assert_bound(a, MLKEM_N, 0, MLKEM_Q);

#if (MLKEM_POLYCOMPRESSEDBYTES_DU == 352)
for (j = 0; j < MLKEM_N / 8; j++)
__loop__(invariant(j <= MLKEM_N / 8))
Expand Down Expand Up @@ -139,6 +141,8 @@ void poly_decompress_du(poly *r, const uint8_t a[MLKEM_POLYCOMPRESSEDBYTES_DU])
#else
#error "MLKEM_POLYCOMPRESSEDBYTES_DU needs to be in {320,352}"
#endif

debug_assert_bound(r, MLKEM_N, 0, MLKEM_Q);
}

MLKEM_NATIVE_INTERNAL_API
Expand Down Expand Up @@ -260,7 +264,6 @@ void poly_tobytes(uint8_t r[MLKEM_POLYBYTES], const poly *a)
unsigned i;
debug_assert_bound(a, MLKEM_N, 0, MLKEM_Q);


for (i = 0; i < MLKEM_N / 2; i++)
__loop__(invariant(i <= MLKEM_N / 2))
{
Expand Down Expand Up @@ -489,7 +492,7 @@ void poly_tomont(poly *r)
for (i = 0; i < MLKEM_N; i++)
__loop__(
invariant(i <= MLKEM_N)
invariant(array_abs_bound(r->coeffs ,0, i, MLKEM_Q)))
invariant(array_abs_bound(r->coeffs, 0, i, MLKEM_Q)))
{
r->coeffs[i] = fqmul(r->coeffs[i], f);
}
Expand Down Expand Up @@ -566,11 +569,20 @@ void poly_mulcache_compute(poly_mulcache *x, const poly *a)
{
unsigned i;
for (i = 0; i < MLKEM_N / 4; i++)
__loop__(invariant(i <= MLKEM_N / 4))
__loop__(
invariant(i <= MLKEM_N / 4)
invariant(array_abs_bound(x->coeffs, 0, 2 * i, MLKEM_Q)))
{
x->coeffs[2 * i + 0] = fqmul(a->coeffs[4 * i + 1], zetas[64 + i]);
x->coeffs[2 * i + 1] = fqmul(a->coeffs[4 * i + 3], -zetas[64 + i]);
}

/*
* This bound is true for the C implementation, but not needed
* in the higher level bounds reasoning. It is thus omitted
* them from the spec to not unnecessarily constrain native
* implementations, but checked here nonetheless.
*/
debug_assert_abs_bound(x, MLKEM_N / 2, MLKEM_Q);
}
#else /* MLKEM_USE_NATIVE_POLY_MULCACHE_COMPUTE */
Expand Down
10 changes: 5 additions & 5 deletions mlkem/poly.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -307,17 +307,17 @@ __contract__(
************************************************************/
static INLINE uint16_t scalar_signed_to_unsigned_q(int16_t c)
__contract__(
requires(c >= -(MLKEM_Q - 1) && c <= (MLKEM_Q - 1))
ensures(return_value >= 0 && return_value <= (MLKEM_Q - 1))
requires(c > -MLKEM_Q && c < MLKEM_Q)
ensures(return_value >= 0 && return_value < MLKEM_Q)
ensures(return_value == (int32_t)c + (((int32_t)c < 0) * MLKEM_Q)))
{
debug_assert_abs_bound(&c, 1, MLKEM_Q);

/* Add Q if c is negative, but in constant time */
c = ct_sel_int16(c + MLKEM_Q, c, ct_cmask_neg_i16(c));

cassert(c >= 0);
cassert(c < MLKEM_Q);

/* and therefore cast to uint16_t is safe. */
debug_assert_bound(&c, 1, 0, MLKEM_Q);
return (uint16_t)c;
}

Expand Down
36 changes: 21 additions & 15 deletions mlkem/polyvec.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ void polyvec_compress_du(uint8_t r[MLKEM_POLYVECCOMPRESSEDBYTES_DU],
const polyvec *a)
{
unsigned i;
debug_assert_bound(a, MLKEM_K * MLKEM_N, 0, MLKEM_Q);
debug_assert_bound_2d(a, MLKEM_K, MLKEM_N, 0, MLKEM_Q);

for (i = 0; i < MLKEM_K; i++)
{
Expand All @@ -33,13 +33,15 @@ void polyvec_decompress_du(polyvec *r,
poly_decompress_du(&r->vec[i], a + i * MLKEM_POLYCOMPRESSEDBYTES_DU);
}

debug_assert_bound(r, MLKEM_K * MLKEM_N, 0, MLKEM_Q);
debug_assert_bound_2d(r, MLKEM_K, MLKEM_N, 0, MLKEM_Q);
}

MLKEM_NATIVE_INTERNAL_API
void polyvec_tobytes(uint8_t r[MLKEM_POLYVECBYTES], const polyvec *a)
{
unsigned i;
debug_assert_bound_2d(a, MLKEM_K, MLKEM_N, 0, MLKEM_Q);

for (i = 0; i < MLKEM_K; i++)
{
poly_tobytes(r + i * MLKEM_POLYBYTES, &a->vec[i]);
Expand All @@ -54,6 +56,8 @@ void polyvec_frombytes(polyvec *r, const uint8_t a[MLKEM_POLYVECBYTES])
{
poly_frombytes(&r->vec[i], a + i * MLKEM_POLYBYTES);
}

debug_assert_bound_2d(r, MLKEM_K, MLKEM_N, 0, UINT12_LIMIT);
}

MLKEM_NATIVE_INTERNAL_API
Expand All @@ -64,6 +68,8 @@ void polyvec_ntt(polyvec *r)
{
poly_ntt(&r->vec[i]);
}

debug_assert_abs_bound_2d(r, MLKEM_K, MLKEM_N, NTT_BOUND);
}

MLKEM_NATIVE_INTERNAL_API
Expand All @@ -74,6 +80,8 @@ void polyvec_invntt_tomont(polyvec *r)
{
poly_invntt_tomont(&r->vec[i]);
}

debug_assert_abs_bound_2d(r, MLKEM_K, MLKEM_N, INVNTT_BOUND);
}

#if !defined(MLKEM_USE_NATIVE_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED)
Expand All @@ -84,37 +92,31 @@ void polyvec_basemul_acc_montgomery_cached(poly *r, const polyvec *a,
{
unsigned i;
poly t;

debug_assert_bound(a, MLKEM_K * MLKEM_N, 0, UINT12_LIMIT);
debug_assert_abs_bound(b, MLKEM_K * MLKEM_N, NTT_BOUND);
debug_assert_abs_bound(b_cache, MLKEM_K * (MLKEM_N / 2), MLKEM_Q);
debug_assert_bound_2d(a, MLKEM_K, MLKEM_N, 0, UINT12_LIMIT);

poly_basemul_montgomery_cached(r, &a->vec[0], &b->vec[0], &b_cache->vec[0]);
for (i = 1; i < MLKEM_K; i++)
{
poly_basemul_montgomery_cached(&t, &a->vec[i], &b->vec[i],
&b_cache->vec[i]);
poly_add(r, &t);
/* abs bounds: < (i+1) * 3/2 * q */
}

/*
* Those bounds are true for the C implementation, but not needed
* in the higher level bounds reasoning. It is thus best to omit
* them from the spec to not unnecessarily constraint native implementations.
* This bound is true for the C implementation, but not needed
* in the higher level bounds reasoning. It is thus omitted
* them from the spec to not unnecessarily constrain native
* implementations, but checked here nonetheless.
*/
cassert(array_abs_bound(r->coeffs, 0, MLKEM_N, MLKEM_K * 2 * MLKEM_Q));
/* TODO: Integrate CBMC assertion into debug_asserts if CBMC is set */
debug_assert_abs_bound(r, MLKEM_N, MLKEM_K * 2 * MLKEM_Q);
debug_assert_abs_bound(r, MLKEM_K, MLKEM_N * 2 * MLKEM_Q);
}
#else /* !MLKEM_USE_NATIVE_POLYVEC_BASEMUL_ACC_MONTGOMERY_CACHED */
MLKEM_NATIVE_INTERNAL_API
void polyvec_basemul_acc_montgomery_cached(poly *r, const polyvec *a,
const polyvec *b,
const polyvec_mulcache *b_cache)
{
debug_assert_bound(a, MLKEM_K * MLKEM_N, 0, UINT12_LIMIT);
debug_assert_abs_bound(b, MLKEM_K * MLKEM_N, NTT_BOUND);
debug_assert_bound_2d(a, MLKEM_K, MLKEM_N, 0, UINT12_LIMIT);
/* Omitting bounds assertion for cache since native implementations may
* decide not to use a mulcache. Note that the C backend implementation
* of poly_basemul_montgomery_cached() does still include the check. */
Expand Down Expand Up @@ -148,6 +150,8 @@ void polyvec_reduce(polyvec *r)
{
poly_reduce(&r->vec[i]);
}

debug_assert_bound_2d(r, MLKEM_K, MLKEM_N, 0, MLKEM_Q);
}

MLKEM_NATIVE_INTERNAL_API
Expand All @@ -168,4 +172,6 @@ void polyvec_tomont(polyvec *r)
{
poly_tomont(&r->vec[i]);
}

debug_assert_abs_bound_2d(r, MLKEM_K, MLKEM_N, MLKEM_Q);
}
Loading

0 comments on commit 79757a2

Please sign in to comment.