Conversation
CBMC Results (ML-DSA-44)Full Results (186 proofs)
|
CBMC Results (ML-DSA-87)
Full Results (186 proofs)
|
CBMC Results (ML-DSA-65)Full Results (186 proofs)
|
| ret = mld_sign_signature(sm, smlen, sm + MLDSA_CRYPTO_BYTES, mlen, ctx, | ||
| ctxlen, sk, context); | ||
| *smlen += mlen; | ||
| if (ret == 0) |
There was a problem hiding this comment.
Please update the comment(s) and the ensures contract for this function in sign.h
(or is it deliberately left under-specified?)
There was a problem hiding this comment.
Do the comments at the top-level API in mldsa/mldsa_native.h also need to be updated?
There was a problem hiding this comment.
I think the contract and comments exactly what we want to guarantee:
(return_value == 0 && *smlen == MLDSA_CRYPTO_BYTES + mlen)
WDYT @hanno-becker?
In the long term I think we should rather consider eliminating smlen altogether - see #789.
There was a problem hiding this comment.
In the failure case(s), should we write *smlen==0 in the ensures clause, or leave it unspecified?
There was a problem hiding this comment.
I'm in favor of harmonizing this with mld_sign_signature, and modify the post-condition from
ensures((return_value == 0 && *smlen == MLDSA_CRYPTO_BYTES + mlen) ||
(return_value == MLD_ERR_FAIL
|| return_value == MLD_ERR_OUT_OF_MEMORY
|| return_value == MLD_ERR_RNG_FAIL))to
ensures((return_value == 0 && *smlen == MLDSA_CRYPTO_BYTES + mlen) ||
((return_value == MLD_ERR_FAIL || return_value == MLD_ERR_OUT_OF_MEMORY || return_value == MLD_ERR_RNG_FAIL) && *smlen == 0))In mld_sign if a failure is returned from mld_sign_signature, we currently set the smlen to mlen (mld_sign_signature returns smlen=0, and we increment it by mlen). This commit changes it so that in the case of failure smlen=0 is returned. Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>
This commit adds a reference to FIPS204 that states that t0 does not need to be considered secret. That replaces an old reference to an eprint report stating the same. Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>
hanno-becker
left a comment
There was a problem hiding this comment.
I agree with @rod-chapman that we should note in the CBMC contract for mld_sign that *smlen == 0 if the function fails.
Uh oh!
There was an error while loading. Please reload this page.