diff --git a/mldsa/mldsa_native.c b/mldsa/mldsa_native.c index 0279b10a3..08eed9aaf 100644 --- a/mldsa/mldsa_native.c +++ b/mldsa/mldsa_native.c @@ -256,9 +256,9 @@ #undef mld_memset /* mldsa/src/packing.h */ #undef MLD_PACKING_H +#undef mld_make_pack_sig_h_poly #undef mld_pack_pk #undef mld_pack_sig_c -#undef mld_pack_sig_h_poly #undef mld_pack_sig_z #undef mld_pack_sk #undef mld_unpack_pk @@ -297,7 +297,6 @@ #undef MLD_POLY_KL_H #undef mld_poly_challenge #undef mld_poly_decompose -#undef mld_poly_make_hint #undef mld_poly_uniform_eta #undef mld_poly_uniform_eta_4x #undef mld_poly_uniform_gamma1 diff --git a/mldsa/mldsa_native_asm.S b/mldsa/mldsa_native_asm.S index 0558fa621..1d3e584ae 100644 --- a/mldsa/mldsa_native_asm.S +++ b/mldsa/mldsa_native_asm.S @@ -261,9 +261,9 @@ #undef mld_memset /* mldsa/src/packing.h */ #undef MLD_PACKING_H +#undef mld_make_pack_sig_h_poly #undef mld_pack_pk #undef mld_pack_sig_c -#undef mld_pack_sig_h_poly #undef mld_pack_sig_z #undef mld_pack_sk #undef mld_unpack_pk @@ -302,7 +302,6 @@ #undef MLD_POLY_KL_H #undef mld_poly_challenge #undef mld_poly_decompose -#undef mld_poly_make_hint #undef mld_poly_uniform_eta #undef mld_poly_uniform_eta_4x #undef mld_poly_uniform_gamma1 diff --git a/mldsa/src/packing.c b/mldsa/src/packing.c index f9cf275a3..06d03daa2 100644 --- a/mldsa/src/packing.c +++ b/mldsa/src/packing.c @@ -8,6 +8,7 @@ #include "packing.h" #include "poly.h" #include "polyvec.h" +#include "rounding.h" /* Parameter set namespacing * This is to facilitate building multiple instances @@ -107,8 +108,9 @@ void mld_pack_sig_c(uint8_t sig[MLDSA_CRYPTO_BYTES], } MLD_INTERNAL_API -void mld_pack_sig_h_poly(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_poly *h, - unsigned int k, unsigned int n) +int mld_make_pack_sig_h_poly(uint8_t sig[MLDSA_CRYPTO_BYTES], + const mld_poly *a0, const mld_poly *a1, + unsigned int k, unsigned int n) { unsigned int j; @@ -119,11 +121,16 @@ void mld_pack_sig_h_poly(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_poly *h, * that are not equal to 0. * * The final K bytes record a running tally of the number of hints - * coming from each of the K polynomials in h. */ + * coming from each of the K polynomials. */ uint8_t *sig_h = sig + MLDSA_CTILDEBYTES + MLDSA_L * MLDSA_POLYZ_PACKEDBYTES; - /* For each coefficient in this polynomial, record it as a hint */ - /* if its value is not zero. */ + /* For each coefficient in this polynomial, compute its hint bit and, if + * non-zero, record the index in the hint section of sig. If recording the + * hint would overflow the OMEGA-sized index array, abort early and return + * MLD_ERR_FAIL. The caller is expected to reject the signature in that case. + * + * Constant time: At this point a0/a1 are public (see comment in sign.c + * before the call), so a data-dependent early return is fine. */ for (j = 0; j < MLDSA_N; j++) __loop__( assigns(j, n, memory_slice(sig_h, MLDSA_POLYVECH_PACKEDBYTES)) @@ -132,12 +139,13 @@ void mld_pack_sig_h_poly(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_poly *h, decreases(MLDSA_N - j) ) { - /* The reference implementation implicitly relies on the total */ - /* number of hints being less than OMEGA, assuming h is valid. */ - /* In mldsa-native, we check this explicitly to ease proof of */ - /* type safety. */ - if (h->coeffs[j] != 0 && n < MLDSA_OMEGA) + const unsigned int hint_bit = mld_make_hint(a0->coeffs[j], a1->coeffs[j]); + if (hint_bit) { + if (n == MLDSA_OMEGA) + { + return MLD_ERR_FAIL; + } sig_h[n] = (uint8_t)j; n++; } @@ -145,6 +153,7 @@ void mld_pack_sig_h_poly(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_poly *h, /* Record the running tally into the correct slot for this */ /* polynomial in the final K bytes. */ sig_h[MLDSA_OMEGA + k] = (uint8_t)n; + return (int)n; } MLD_INTERNAL_API diff --git a/mldsa/src/packing.h b/mldsa/src/packing.h index 0479c09a9..da850219b 100644 --- a/mldsa/src/packing.h +++ b/mldsa/src/packing.h @@ -87,29 +87,41 @@ __contract__( assigns(memory_slice(sig, MLDSA_CRYPTO_BYTES)) ); -#define mld_pack_sig_h_poly MLD_NAMESPACE_KL(pack_sig_h_poly) +#define mld_make_pack_sig_h_poly MLD_NAMESPACE_KL(make_pack_sig_h_poly) /************************************************* - * Name: mld_pack_sig_h_poly + * Name: mld_make_pack_sig_h_poly * - * Description: Pack hints for one polynomial into the hint section of sig. + * Description: Compute hints for one polynomial of (w0, w1) and pack them + * into the hint section of sig. * Must be called once per polynomial in order k = 0, ..., K-1. * The hint section of sig must be zeroed before the first call. * * Arguments: - uint8_t sig[]: byte array containing signature - * - const mld_poly *h: pointer to hint polynomial (0/1 coeffs) + * - const mld_poly *a0: pointer to low part of input polynomial + * - const mld_poly *a1: pointer to high part of input polynomial * - unsigned int k: index of polynomial in vector (0..K-1) * - unsigned int n: total number of hints written so far + * + * Returns: - the updated running tally of hints (non-negative, at most + * MLDSA_OMEGA) on success; + * - MLD_ERR_FAIL if writing all hints for this polynomial + * would exceed MLDSA_OMEGA. In this case the caller must + * reject the signature. **************************************************/ MLD_INTERNAL_API -void mld_pack_sig_h_poly(uint8_t sig[MLDSA_CRYPTO_BYTES], const mld_poly *h, - unsigned int k, unsigned int n) +MLD_MUST_CHECK_RETURN_VALUE +int mld_make_pack_sig_h_poly(uint8_t sig[MLDSA_CRYPTO_BYTES], + const mld_poly *a0, const mld_poly *a1, + unsigned int k, unsigned int n) __contract__( requires(memory_no_alias(sig, MLDSA_CRYPTO_BYTES)) - requires(memory_no_alias(h, sizeof(mld_poly))) + requires(memory_no_alias(a0, sizeof(mld_poly))) + requires(memory_no_alias(a1, sizeof(mld_poly))) requires(k < MLDSA_K) requires(n <= MLDSA_OMEGA) - requires(array_bound(h->coeffs, 0, MLDSA_N, 0, 2)) assigns(memory_slice(sig, MLDSA_CRYPTO_BYTES)) + ensures(return_value == MLD_ERR_FAIL || + (return_value >= 0 && return_value <= MLDSA_OMEGA)) ); #define mld_pack_sig_z MLD_NAMESPACE_KL(pack_sig_z) @@ -118,7 +130,7 @@ __contract__( * * Description: Bit-pack single polynomial of z component of sig = (c, z, h). * The c and h components are packed separately using - * mld_pack_sig_c and mld_pack_sig_h_poly. + * mld_pack_sig_c and mld_make_pack_sig_h_poly. * * Arguments: - uint8_t sig[]: output byte array * - const mld_poly *zi: pointer to a single polynomial in z diff --git a/mldsa/src/poly_kl.c b/mldsa/src/poly_kl.c index 84ae53a7e..327536156 100644 --- a/mldsa/src/poly_kl.c +++ b/mldsa/src/poly_kl.c @@ -100,30 +100,6 @@ void mld_poly_decompose(mld_poly *a1, mld_poly *a0) mld_poly_decompose_c(a1, a0); } -MLD_INTERNAL_API -unsigned int mld_poly_make_hint(mld_poly *h, const mld_poly *a0, - const mld_poly *a1) -{ - unsigned int i, s = 0; - - for (i = 0; i < MLDSA_N; ++i) - __loop__( - invariant(i <= MLDSA_N) - invariant(s <= i) - invariant(array_bound(h->coeffs, 0, i, 0, 2)) - decreases(MLDSA_N - i) - ) - { - const unsigned int hint_bit = mld_make_hint(a0->coeffs[i], a1->coeffs[i]); - h->coeffs[i] = (int32_t)hint_bit; - s += hint_bit; - } - - mld_assert(s <= MLDSA_N); - mld_assert_bound(h->coeffs, MLDSA_N, 0, 2); - return s; -} - MLD_STATIC_TESTABLE void mld_poly_use_hint_c(mld_poly *b, const mld_poly *a, const mld_poly *h) __contract__( diff --git a/mldsa/src/poly_kl.h b/mldsa/src/poly_kl.h index a7c71707d..1518fe2d8 100644 --- a/mldsa/src/poly_kl.h +++ b/mldsa/src/poly_kl.h @@ -43,33 +43,6 @@ __contract__( ); -#define mld_poly_make_hint MLD_NAMESPACE_KL(poly_make_hint) -/************************************************* - * Name: mld_poly_make_hint - * - * Description: Compute hint polynomial. The coefficients of which indicate - * whether the low bits of the corresponding coefficient of - * the input polynomial overflow into the high bits. - * - * Arguments: - mld_poly *h: pointer to output hint polynomial - * - const mld_poly *a0: pointer to low part of input polynomial - * - const mld_poly *a1: pointer to high part of input polynomial - * - * Returns number of 1 bits. - **************************************************/ -MLD_INTERNAL_API -MLD_MUST_CHECK_RETURN_VALUE -unsigned int mld_poly_make_hint(mld_poly *h, const mld_poly *a0, - const mld_poly *a1) -__contract__( - requires(memory_no_alias(h, sizeof(mld_poly))) - requires(memory_no_alias(a0, sizeof(mld_poly))) - requires(memory_no_alias(a1, sizeof(mld_poly))) - assigns(memory_slice(h, sizeof(mld_poly))) - ensures(return_value <= MLDSA_N) - ensures(array_bound(h->coeffs, 0, MLDSA_N, 0, 2)) -); - #define mld_poly_use_hint MLD_NAMESPACE_KL(poly_use_hint) /************************************************* * Name: mld_poly_use_hint diff --git a/mldsa/src/sign.c b/mldsa/src/sign.c index 4b15b1a50..7a41d7e85 100644 --- a/mldsa/src/sign.c +++ b/mldsa/src/sign.c @@ -728,22 +728,18 @@ __contract__( n = 0; for (k = 0; k < MLDSA_K; k++) __loop__( - assigns(k, n, - memory_slice(z, sizeof(mld_poly)), - memory_slice(sig, MLDSA_CRYPTO_BYTES)) + assigns(k, n, ret, memory_slice(sig, MLDSA_CRYPTO_BYTES)) invariant(k <= MLDSA_K) invariant(n <= MLDSA_OMEGA) decreases(MLDSA_K - k) ) { - unsigned int hints = mld_poly_make_hint(z, &w0->vec[k], &w1->vec[k]); - if (n + hints > MLDSA_OMEGA) + ret = mld_make_pack_sig_h_poly(sig, &w0->vec[k], &w1->vec[k], k, n); + if (ret == MLD_ERR_FAIL) { - ret = MLD_ERR_FAIL; /* reject */ goto cleanup; } - mld_pack_sig_h_poly(sig, z, k, n); - n += hints; + n = (unsigned int)ret; } /* Constant time: At this point it is clear that the signature is valid - it diff --git a/proofs/cbmc/attempt_signature_generation/Makefile b/proofs/cbmc/attempt_signature_generation/Makefile index ebf0a15bb..903c84211 100644 --- a/proofs/cbmc/attempt_signature_generation/Makefile +++ b/proofs/cbmc/attempt_signature_generation/Makefile @@ -37,9 +37,8 @@ USE_FUNCTION_CONTRACTS+=mld_poly_sub USE_FUNCTION_CONTRACTS+=mld_poly_reduce USE_FUNCTION_CONTRACTS+=mld_poly_chknorm USE_FUNCTION_CONTRACTS+=mld_poly_add -USE_FUNCTION_CONTRACTS+=mld_poly_make_hint USE_FUNCTION_CONTRACTS+=mld_pack_sig_c -USE_FUNCTION_CONTRACTS+=mld_pack_sig_h_poly +USE_FUNCTION_CONTRACTS+=mld_make_pack_sig_h_poly USE_FUNCTION_CONTRACTS+=mld_zeroize APPLY_LOOP_CONTRACTS=on diff --git a/proofs/cbmc/pack_sig_h_poly/Makefile b/proofs/cbmc/make_pack_sig_h_poly/Makefile similarity index 90% rename from proofs/cbmc/pack_sig_h_poly/Makefile rename to proofs/cbmc/make_pack_sig_h_poly/Makefile index 700ac1ef8..db73b4033 100644 --- a/proofs/cbmc/pack_sig_h_poly/Makefile +++ b/proofs/cbmc/make_pack_sig_h_poly/Makefile @@ -4,11 +4,11 @@ include ../Makefile_params.common HARNESS_ENTRY = harness -HARNESS_FILE = pack_sig_h_poly_harness +HARNESS_FILE = make_pack_sig_h_poly_harness # This should be a unique identifier for this proof, and will appear on the # Litani dashboard. It can be human-readable and contain spaces if you wish. -PROOF_UID = pack_sig_h_poly +PROOF_UID = make_pack_sig_h_poly DEFINES += INCLUDES += @@ -19,8 +19,8 @@ UNWINDSET += PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/src/packing.c -CHECK_FUNCTION_CONTRACTS=mld_pack_sig_h_poly -USE_FUNCTION_CONTRACTS= +CHECK_FUNCTION_CONTRACTS=mld_make_pack_sig_h_poly +USE_FUNCTION_CONTRACTS=mld_make_hint APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 @@ -29,7 +29,7 @@ EXTERNAL_SAT_SOLVER= CBMCFLAGS=--external-smt2-solver $(PROOF_ROOT)/lib/z3_no_bv_extract --z3 CBMCFLAGS+=--slice-formula -FUNCTION_NAME = pack_sig_h_poly +FUNCTION_NAME = make_pack_sig_h_poly # If this proof is found to consume huge amounts of RAM, you can set the # EXPENSIVE variable. With new enough versions of the proof tools, this will diff --git a/proofs/cbmc/pack_sig_h_poly/pack_sig_h_poly_harness.c b/proofs/cbmc/make_pack_sig_h_poly/make_pack_sig_h_poly_harness.c similarity index 69% rename from proofs/cbmc/pack_sig_h_poly/pack_sig_h_poly_harness.c rename to proofs/cbmc/make_pack_sig_h_poly/make_pack_sig_h_poly_harness.c index 3dd840a4e..c696084ba 100644 --- a/proofs/cbmc/pack_sig_h_poly/pack_sig_h_poly_harness.c +++ b/proofs/cbmc/make_pack_sig_h_poly/make_pack_sig_h_poly_harness.c @@ -6,7 +6,8 @@ void harness(void) { uint8_t *sig; - mld_poly *h; + mld_poly *a0, *a1; unsigned int k, n; - mld_pack_sig_h_poly(sig, h, k, n); + int r; + r = mld_make_pack_sig_h_poly(sig, a0, a1, k, n); } diff --git a/proofs/cbmc/poly_make_hint/Makefile b/proofs/cbmc/poly_make_hint/Makefile deleted file mode 100644 index f2b061e80..000000000 --- a/proofs/cbmc/poly_make_hint/Makefile +++ /dev/null @@ -1,55 +0,0 @@ -# Copyright (c) The mldsa-native project authors -# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT - -include ../Makefile_params.common - -HARNESS_ENTRY = harness -HARNESS_FILE = poly_make_hint_harness - -# This should be a unique identifier for this proof, and will appear on the -# Litani dashboard. It can be human-readable and contain spaces if you wish. -PROOF_UID = poly_make_hint - -DEFINES += -INCLUDES += - -REMOVE_FUNCTION_BODY += -UNWINDSET += - -PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c -PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly_kl.c - -CHECK_FUNCTION_CONTRACTS=mld_poly_make_hint -USE_FUNCTION_CONTRACTS=mld_make_hint -APPLY_LOOP_CONTRACTS=on -USE_DYNAMIC_FRAMES=1 - -# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead -EXTERNAL_SAT_SOLVER= -CBMCFLAGS=--smt2 - -FUNCTION_NAME = poly_make_hint - -# If this proof is found to consume huge amounts of RAM, you can set the -# EXPENSIVE variable. With new enough versions of the proof tools, this will -# restrict the number of EXPENSIVE CBMC jobs running at once. See the -# documentation in Makefile.common under the "Job Pools" heading for details. -# EXPENSIVE = true - -# This function is large enough to need... -CBMC_OBJECT_BITS = 8 - -# If you require access to a file-local ("static") function or object to conduct -# your proof, set the following (and do not include the original source file -# ("mldsa/poly.c") in PROJECT_SOURCES). -# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i -# include ../Makefile.common -# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/src/poly.c -# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar -# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz -# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must -# be set before including Makefile.common, but any use of variables on the -# left-hand side requires those variables to be defined. Hence, _SOURCE, -# _FUNCTIONS, _OBJECTS is set after including Makefile.common. - -include ../Makefile.common diff --git a/proofs/cbmc/poly_make_hint/poly_make_hint_harness.c b/proofs/cbmc/poly_make_hint/poly_make_hint_harness.c deleted file mode 100644 index fc03487dc..000000000 --- a/proofs/cbmc/poly_make_hint/poly_make_hint_harness.c +++ /dev/null @@ -1,11 +0,0 @@ -// Copyright (c) The mldsa-native project authors -// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT - -#include "poly_kl.h" - -void harness(void) -{ - mld_poly *a, *b, *c; - unsigned int r; - r = mld_poly_make_hint(a, b, c); -}