From 97b77c7dc3b240d3511dd9218c247c969c7c68ac Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Thu, 31 Oct 2024 06:53:45 +0000 Subject: [PATCH 1/2] Strengthen specification for montgomery_reduce() There are two uses of the generic Montgomery reduction `montgomery_reduce()` in the code base: - For modular multiplication with twiddles in `fqmul()` - For Montgomery reduction after accumulation in the base multiplication. Those two uses require different specifications for `montgomery_reduce()`. However, there does not appear to be a mechanism in CBMC to register more than one contract. To remedy, this commit moves the previous `montgomery_reduce()` into a static inline `montgomery_reduce_generic()`, and uses it in the definitions of `montgomery_reduce()` and `fqmul()`. The new `montgomery_reduce()` then makes bounds assumptions according to the use in base multiplication, while the call to `fqmul()` provides stronger input bounds. Accordingly, the post-condition of `montgomery_reduce()` only guarantees coefficients < 3/2q, while `fqmul()` ensures < q. The CBMC contracts an proofs for `montgomery_reduce()` and `fqmul()` are adjusted accordingly. Signed-off-by: Hanno Becker --- cbmc/proofs/fqmul/Makefile | 4 ++-- mlkem/common.h | 1 + mlkem/reduce.c | 25 ++++++++++++++++++++++--- mlkem/reduce.h | 37 ++++++++++++++++++++++++------------- 4 files changed, 49 insertions(+), 18 deletions(-) diff --git a/cbmc/proofs/fqmul/Makefile b/cbmc/proofs/fqmul/Makefile index f0b1dd2ae..a350c0d51 100644 --- a/cbmc/proofs/fqmul/Makefile +++ b/cbmc/proofs/fqmul/Makefile @@ -18,8 +18,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mlkem/reduce.c -CHECK_FUNCTION_CONTRACTS=fqmul -USE_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)montgomery_reduce +CHECK_FUNCTION_CONTRACTS=$(MLKEM_NAMESPACE)fqmul +USE_FUNCTION_CONTRACTS= APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 diff --git a/mlkem/common.h b/mlkem/common.h index de38a215b..d7ac86d6d 100644 --- a/mlkem/common.h +++ b/mlkem/common.h @@ -4,5 +4,6 @@ #define DEFAULT_ALIGN 32 #define ALIGN __attribute__((aligned(DEFAULT_ALIGN))) +#define ALWAYS_INLINE __attribute__((always_inline)) #endif diff --git a/mlkem/reduce.c b/mlkem/reduce.c index 2b8fdd0e7..18ec83207 100644 --- a/mlkem/reduce.c +++ b/mlkem/reduce.c @@ -33,9 +33,9 @@ static inline int16_t cast_uint16_to_int16(uint16_t x) { #endif /************************************************* - * Name: montgomery_reduce + * Name: montgomery_reduce_generic * - * Description: Montgomery reduction; given a 32-bit integer a, computes + * Description: Generic Montgomery reduction; given a 32-bit integer a, computes * 16-bit integer congruent to a * R^-1 mod q, where R=2^16 * * Arguments: - int32_t a: input integer to be reduced @@ -56,7 +56,8 @@ static inline int16_t cast_uint16_to_int16(uint16_t x) { * < C with a value of abs < q has absolute value * < q (C/2^16 + 1/2). **************************************************/ -int16_t montgomery_reduce(int32_t a) { +ALWAYS_INLINE +static inline int16_t montgomery_reduce_generic(int32_t a) { // Bounds on paper // // - Case |a| < q * C, for some C @@ -87,6 +88,24 @@ int16_t montgomery_reduce(int32_t a) { return (int16_t)r; } +int16_t montgomery_reduce(int32_t a) { + SCALAR_BOUND(a, 2 * MLKEM_Q * 32768, "montgomery_reduce input"); + + int16_t res = montgomery_reduce_generic(a); + + SCALAR_BOUND(res, (3 * (MLKEM_Q + 1)) / 2, "montgomery_reduce output"); + return res; +} + +int16_t fqmul(int16_t a, int16_t b) { + SCALAR_BOUND(b, HALF_Q, "fqmul input"); + + int16_t res = montgomery_reduce((int32_t)a * (int32_t)b); + + SCALAR_BOUND(res, MLKEM_Q, "fqmul output"); + return res; +} + // To divide by MLKEM_Q using Barrett multiplication, the "magic number" // multiplier is round_to_nearest(2**26/MLKEM_Q) #define BPOWER 26 diff --git a/mlkem/reduce.h b/mlkem/reduce.h index 110b32f8f..f07ee9335 100644 --- a/mlkem/reduce.h +++ b/mlkem/reduce.h @@ -8,26 +8,37 @@ #include "params.h" #define MONT -1044 // 2^16 mod q -#define HALF_Q ((MLKEM_Q - 1) / 2) // 1664 +#define HALF_Q ((MLKEM_Q + 1) / 2) // 1665 +/************************************************* + * Name: montgomery_reduce + * + * Description: Montgomery reduction + * + * Arguments: - int32_t a: input integer to be reduced + * Must be smaller than 2 * q * 2^15 in absolute value. + * + * Returns: integer congruent to a * R^-1 modulo q, + * smaller than 3/2 q in absolute value. + **************************************************/ #define montgomery_reduce MLKEM_NAMESPACE(montgomery_reduce) int16_t montgomery_reduce(int32_t a) // clang-format off -REQUIRES(a >= INT32_MIN + (32768 * MLKEM_Q)) -REQUIRES(a <= INT32_MAX - (32768 * MLKEM_Q)) -ENSURES(RETURN_VALUE >= INT16_MIN && RETURN_VALUE <= INT16_MAX); +REQUIRES(a > -(2 * MLKEM_Q * 32768)) +REQUIRES(a < (2 * MLKEM_Q * 32768)) +ENSURES(RETURN_VALUE > -(3 * HALF_Q) && RETURN_VALUE < (3 * HALF_Q)); // clang-format on #define barrett_reduce MLKEM_NAMESPACE(barrett_reduce) int16_t barrett_reduce(int16_t a) // clang-format off -ENSURES(RETURN_VALUE >= -HALF_Q && RETURN_VALUE <= HALF_Q); +ENSURES(RETURN_VALUE > -HALF_Q && RETURN_VALUE < HALF_Q); // clang-format on /************************************************* * Name: fqmul * - * Description: Multiplication followed by Montgomery reduction + * Description: Montgomery multiplication modulo q=3329 * * Arguments: - int16_t a: first factor * Can be any int16_t. @@ -38,13 +49,13 @@ ENSURES(RETURN_VALUE >= -HALF_Q && RETURN_VALUE <= HALF_Q); * smaller than q in absolute value. * **************************************************/ -static inline int16_t fqmul(int16_t a, int16_t b) { - SCALAR_BOUND(b, HALF_Q + 1, "fqmul input"); - - int16_t res = montgomery_reduce((int32_t)a * (int32_t)b); +#define fqmul MLKEM_NAMESPACE(fqmul) +int16_t fqmul(int16_t a, int16_t b) + // clang-format off +REQUIRES(b > -HALF_Q) +REQUIRES(b < HALF_Q) +ENSURES(RETURN_VALUE > -MLKEM_Q && RETURN_VALUE < MLKEM_Q); +// clang-format on - SCALAR_BOUND(res, MLKEM_Q, "fqmul output"); - return res; -} #endif From b3f89d8978330b4349ef80fc82b3c14e0a22bcba Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Thu, 31 Oct 2024 16:57:04 +0000 Subject: [PATCH 2/2] Avoid non-integral quotient in documentation of fqmul() fqmul() is documented to require a 2nd input that's "< q/2" in absolute value. This is the correct meaning when reading q/2 as a _rational_ quotient, but it's not when q/2 is read as round-down division: In that case, one would need to say <= instead of <. This commit avoids any confusion by rewriting the documentation in terms of the integral quotient (q+1)/2. Signed-off-by: Hanno Becker --- mlkem/reduce.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mlkem/reduce.h b/mlkem/reduce.h index f07ee9335..1322fc353 100644 --- a/mlkem/reduce.h +++ b/mlkem/reduce.h @@ -43,7 +43,7 @@ ENSURES(RETURN_VALUE > -HALF_Q && RETURN_VALUE < HALF_Q); * Arguments: - int16_t a: first factor * Can be any int16_t. * - int16_t b: second factor. - * Must be signed canonical (abs value <|q|/2) + * Must be signed canonical (abs value <(q+1)/2) * * Returns 16-bit integer congruent to a*b*R^{-1} mod q, and * smaller than q in absolute value.