From d3c3dc1174afd823d9c90d719080c6e6a38a8efc Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Mon, 1 Dec 2025 14:31:04 +0800 Subject: [PATCH 1/2] CT: Align ct_sel_int32 with mlkem-native ct_sel_int32 in mldsa-native previously had a precondition that the condition is either 0 or 0xFFFFFFFF. This is different from mlkem-native where any value is permitted for mlk_ct_sel_int16. This commit aligns ct_sel_int32 with mlkem-native. Signed-off-by: Matthias J. Kannwischer --- mldsa/src/ct.h | 19 ++++++- proofs/cbmc/ct_cmask_nonzero_u32/Makefile | 55 +++++++++++++++++++ .../ct_cmask_nonzero_u32_harness.c | 10 ++++ proofs/cbmc/ct_sel_int32/Makefile | 2 +- 4 files changed, 83 insertions(+), 3 deletions(-) create mode 100644 proofs/cbmc/ct_cmask_nonzero_u32/Makefile create mode 100644 proofs/cbmc/ct_cmask_nonzero_u32/ct_cmask_nonzero_u32_harness.c diff --git a/mldsa/src/ct.h b/mldsa/src/ct.h index 1975ebf82..d3040c508 100644 --- a/mldsa/src/ct.h +++ b/mldsa/src/ct.h @@ -190,6 +190,22 @@ static MLD_ALWAYS_INLINE uint32_t mld_cast_int32_to_uint32(int32_t x) return mld_cast_int64_to_uint32((int64_t)x); } +/************************************************* + * Name: mld_ct_cmask_nonzero_u32 + * + * Description: Return 0 if input is zero, and -1 otherwise. + * + * Arguments: uint32_t x: Value to be converted into a mask + * + **************************************************/ +static MLD_INLINE uint32_t mld_ct_cmask_nonzero_u32(uint32_t x) +__contract__(ensures(return_value == ((x == 0) ? 0 : 0xFFFFFFFF))) +{ + int64_t tmp = mld_value_barrier_i64(-((int64_t)x)); + tmp >>= 32; + return mld_cast_int64_to_uint32(tmp); +} + /************************************************* * Name: mld_ct_sel_int32 * @@ -205,13 +221,12 @@ static MLD_ALWAYS_INLINE uint32_t mld_cast_int32_to_uint32(int32_t x) **************************************************/ static MLD_INLINE int32_t mld_ct_sel_int32(int32_t a, int32_t b, uint32_t cond) __contract__( - requires(cond == 0x0 || cond == 0xFFFFFFFF) ensures(return_value == (cond ? a : b)) ) { uint32_t au = mld_cast_int32_to_uint32(a); uint32_t bu = mld_cast_int32_to_uint32(b); - uint32_t res = bu ^ (mld_value_barrier_u32(cond) & (au ^ bu)); + uint32_t res = bu ^ (mld_ct_cmask_nonzero_u32(cond) & (au ^ bu)); return mld_cast_uint32_to_int32(res); } diff --git a/proofs/cbmc/ct_cmask_nonzero_u32/Makefile b/proofs/cbmc/ct_cmask_nonzero_u32/Makefile new file mode 100644 index 000000000..d93c9e9f6 --- /dev/null +++ b/proofs/cbmc/ct_cmask_nonzero_u32/Makefile @@ -0,0 +1,55 @@ +# 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 = ct_cmask_nonzero_u32_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 = mld_ct_cmask_nonzero_u32 + +DEFINES += -DMLD_CONFIG_NO_ASM_VALUE_BARRIER +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/mldsa/src/ct.c + +CHECK_FUNCTION_CONTRACTS=mld_ct_cmask_nonzero_u32 +USE_FUNCTION_CONTRACTS=mld_value_barrier_i64 +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 = mld_ct_cmask_nonzero_u32 + +# 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/ct_cmask_nonzero_u32/ct_cmask_nonzero_u32_harness.c b/proofs/cbmc/ct_cmask_nonzero_u32/ct_cmask_nonzero_u32_harness.c new file mode 100644 index 000000000..3a742de43 --- /dev/null +++ b/proofs/cbmc/ct_cmask_nonzero_u32/ct_cmask_nonzero_u32_harness.c @@ -0,0 +1,10 @@ +// Copyright (c) The mldsa-native project authors +// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT + +#include "ct.h" + +void harness(void) +{ + uint32_t cond; + mld_ct_cmask_nonzero_u32(cond); +} diff --git a/proofs/cbmc/ct_sel_int32/Makefile b/proofs/cbmc/ct_sel_int32/Makefile index 76d76b470..6dd4548e9 100644 --- a/proofs/cbmc/ct_sel_int32/Makefile +++ b/proofs/cbmc/ct_sel_int32/Makefile @@ -20,7 +20,7 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c PROJECT_SOURCES += $(SRCDIR)/mldsa/src/ct.c CHECK_FUNCTION_CONTRACTS=mld_ct_sel_int32 -USE_FUNCTION_CONTRACTS=mld_value_barrier_u32 +USE_FUNCTION_CONTRACTS=mld_ct_cmask_nonzero_u32 APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1 From 9afc7b0f244bd7029efe2f9ca6196f38dd968d57 Mon Sep 17 00:00:00 2001 From: "Matthias J. Kannwischer" Date: Fri, 28 Nov 2025 18:12:29 +0800 Subject: [PATCH 2/2] verify: Switch to constant-time memcmp In the very end of verify one has to compare the input challenge to the re-computed challenge. If they are equal (and some previous checks on h and z passed), the signature is valid. Currently, our constant-time tests do not declassify the message and we, hence, need to declassify in this final step. Before thi commit, the declassification would happen on the recomputed challenge just before the memcmp. Now that a constant-time memcmp was added in https://github.com/pq-code-package/mldsa-native/pull/714, we might as well use that; that plus a constant-time selections allows us to not use any declassifications in verification, i.e., we do not leak the verification result through timing. Signed-off-by: Matthias J. Kannwischer --- mldsa/src/sign.c | 34 +++++-------------- .../cbmc/crypto_sign_verify_internal/Makefile | 2 ++ 2 files changed, 11 insertions(+), 25 deletions(-) diff --git a/mldsa/src/sign.c b/mldsa/src/sign.c index 86e318fb6..710a3b653 100644 --- a/mldsa/src/sign.c +++ b/mldsa/src/sign.c @@ -782,7 +782,6 @@ int crypto_sign_verify_internal(const uint8_t *sig, size_t siglen, const uint8_t pk[CRYPTO_PUBLICKEYBYTES], int externalmu) { - unsigned int i; int res; MLD_ALIGN uint8_t buf[MLDSA_K * MLDSA_POLYW1_PACKEDBYTES]; MLD_ALIGN uint8_t rho[MLDSA_SEEDBYTES]; @@ -853,28 +852,8 @@ int crypto_sign_verify_internal(const uint8_t *sig, size_t siglen, mld_H(c2, MLDSA_CTILDEBYTES, mu, MLDSA_CRHBYTES, buf, MLDSA_K * MLDSA_POLYW1_PACKEDBYTES, NULL, 0); - /* Constant time: All data in verification is usually considered public. - * However, in our constant-time tests we do not declassify the message and - * context string. - * The following conditional is the only place in verification whose run-time - * depends on the message. As all that can be leakaged here is the output of - * a hash call (that should behave like a random oracle), it is safe to - * declassify here even with a secret message. - */ - MLD_CT_TESTING_DECLASSIFY(c2, sizeof(c2)); - for (i = 0; i < MLDSA_CTILDEBYTES; ++i) - __loop__( - invariant(i <= MLDSA_CTILDEBYTES) - ) - { - if (c[i] != c2[i]) - { - res = -1; - goto cleanup; - } - } - - res = 0; + /* Return 0 if c == c2, -1 otherwise */ + res = mld_ct_sel_int32(-1, 0, mld_ct_memcmp(c, c2, MLDSA_CTILDEBYTES)); cleanup: /* @[FIPS204, Section 3.6.3] Destruction of intermediate values. */ @@ -938,6 +917,7 @@ int crypto_sign_open(uint8_t *m, size_t *mlen, const uint8_t *sm, size_t smlen, const uint8_t pk[CRYPTO_PUBLICKEYBYTES]) { size_t i; + int result; if (smlen < CRYPTO_BYTES) { @@ -945,8 +925,12 @@ int crypto_sign_open(uint8_t *m, size_t *mlen, const uint8_t *sm, size_t smlen, } *mlen = smlen - CRYPTO_BYTES; - if (crypto_sign_verify(sm, CRYPTO_BYTES, sm + CRYPTO_BYTES, *mlen, ctx, - ctxlen, pk)) + result = crypto_sign_verify(sm, CRYPTO_BYTES, sm + CRYPTO_BYTES, *mlen, ctx, + ctxlen, pk); + /* Declassify the final result of the verification. */ + /* TODO: Consider making open constant flow */ + MLD_CT_TESTING_DECLASSIFY(&result, sizeof(result)); + if (result) { goto badsig; } diff --git a/proofs/cbmc/crypto_sign_verify_internal/Makefile b/proofs/cbmc/crypto_sign_verify_internal/Makefile index 38e469764..c3e7ea201 100644 --- a/proofs/cbmc/crypto_sign_verify_internal/Makefile +++ b/proofs/cbmc/crypto_sign_verify_internal/Makefile @@ -39,6 +39,8 @@ USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_caddq USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_use_hint USE_FUNCTION_CONTRACTS+=$(MLD_NAMESPACE)polyveck_pack_w1 USE_FUNCTION_CONTRACTS+=mld_zeroize +USE_FUNCTION_CONTRACTS+=mld_ct_memcmp +USE_FUNCTION_CONTRACTS+=mld_ct_sel_int32 APPLY_LOOP_CONTRACTS=on USE_DYNAMIC_FRAMES=1