Add missing secret key coefficient validation

[sgmenda]

Issues:

crypto_sign_pk_from_sk was not verifying that s1 and s2 polynomial coefficients were within the valid range [-η, η].

Description of changes:

Implements missing validation in crypto_sign_pk_from_sk to verify that s1 and s2 polynomial coefficients are within the valid range [-η, η].

Motivated by aws/aws-lc#2874 where we discovered, via a Wycheproof test vector, that AWS-LC's MLDSA implementation was accepting secret keys with out-of-bounds s1/s2 coefficients.

Call-outs:

• Covers all three MLDSA parameter sets (44, 65, 87) and both s1 and s2 polynomial vectors
• Tests both underflow and overflow conditions at key boundary positions (first/last coefficients and polynomials)

Testing:

The new functional tests and the existing tests all pass.

make run_func
make run_unit
make run_kat

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license and the ISC license.

[hanno-becker]

Thank you @sgmenda for raising this!

I see that in aws/aws-lc#2874 you added the check to ml_dsa_pack_pk_from_sk. How did you evaluate where to put it?

It seems to depend on the assumptions we make on the input. If we assume a valid SK, then the check is not needed. If we don't assume a valid SK, then why do we only surface the validity issue in a ml_dsa_pack_pk_from_sk, rather than a standalone function checking (aspects of) SK validity?

Does the spec say something about this check?

EDIT: Oh well, I should have read our own documentation first. It clearly says that pack_pk_from_sk does contain SK validation.

[sgmenda]

@hanno-becker yep, exactly. crypto_sign_pk_from_sk already does validation like recomputing the hash, but is missing this particular check.

mldsa-native/mldsa/mldsa_native.h

Lines 672 to 685 in b7e9a26

	/*************************************************
	* Name: crypto_sign_pk_from_sk
	*
	* Description: Derives public key from secret key with validation.
	* Checks that t0 and tr stored in sk match recomputed values.
	*
	* Arguments: - uint8_t pk[CRYPTO_PUBLICKEYBYTES]: output public key
	* - const uint8_t sk[CRYPTO_SECRETKEYBYTES]: input secret key
	*
	* Returns 0 on success, -1 if validation fails (invalid secret key)
	*
	* Note: This function leaks whether the secret key is valid or invalid
	* through its return value and timing.
	**************************************************/

[jakemas]

Thank you for this! In my mind, my first thought was to modify the function mld_unpack_sk/mld_polyvecl_unpack_eta to perform the bounds check within this function itself -- the consequences of said approach would effect much more of the implementation as a whole, of course. I'll explain by thinking below:

In my mind, the fundamental issue is this function: https://github.com/pq-code-package/mldsa-native/blob/main/mldsa/src/polyvec.h#L666-L685

/*************************************************
 * Name:        mld_polyvecl_unpack_eta
 *
 * Description: Unpack polynomial vector with coefficients in
 *              [-MLDSA_ETA,MLDSA_ETA].
 *
 * Arguments:   - mld_polyvecl *p: pointer to output polynomial vector
 *              - const uint8_t *r: input byte array with
 *                                  bit-packed polynomial vector
 **************************************************/
MLD_INTERNAL_API
void mld_polyvecl_unpack_eta(
    mld_polyvecl *p, const uint8_t r[MLDSA_L * MLDSA_POLYETA_PACKEDBYTES])
__contract__(
  requires(memory_no_alias(r,  MLDSA_L * MLDSA_POLYETA_PACKEDBYTES))
  requires(memory_no_alias(p, sizeof(mld_polyvecl)))
  assigns(memory_slice(p, sizeof(mld_polyvecl)))
  ensures(forall(k1, 0, MLDSA_L,
    array_bound(p->vec[k1].coeffs, 0, MLDSA_N, MLD_POLYETA_UNPACK_LOWER_BOUND, MLDSA_ETA + 1)))
);

Should not be bound to MLD_POLYETA_UNPACK_LOWER_BOUND, but by MLDSA_ETA itself. We made this modification in cf01977 see:

/*
 * polyeta_unpack produces coefficients in [-MLDSA_ETA,MLDSA_ETA] for
 * well-formed inputs (i.e., those produced by polyeta_pack).
 * However, when passed an arbitrary byte array, it may produce smaller values,
 * i.e, values in [MLD_POLYETA_UNPACK_LOWER_BOUND,MLDSA_ETA]
 * Even though this should never happen, we use use the bound for arbitrary
 * inputs in the CBMC proofs.
 */

Essentially, what I feel the crux of this PR is getting at, is changing the above decision for polyeta_unpack to use the bounds for well-formed inputs, and fail on the "arbitrary input" bound. What are thoughts on this? It seems the CBMC highlighted this little intricate area of the code well. Rather than widen it the CBMC contract to MLD_POLYETA_UNPACK_LOWER_BOUND, we take it back to +-MLDSA_ETA and then, perform the bounds check here, we get polyeta_unpack to fail if outside the range, thus appeasing the CBMC contract at the correct range.

The current approach in this PR solves the issue in a way I hadn't first considered, and I just want to know the pros/cons of this over allowing polyeta_pack to unpack outside of MLDSA_ETA range. By validating at the lowest level, we wouldn't have to do any validation further up the calling line, we'd know that polyeta_pack couldn't produce invalid keys like this (seems like what the CBMC contract should be doing?).

This all came to me when creating the CBMC contract for the pk_from_sk function, I had to make the bounds (in a previous design iteration) use MLD_POLYETA_UNPACK_LOWER_BOUND rather than MLDSA_ETA, and chased the history down.