Avoid mismatched comparison and fix error in forall/exists macros

[nmouha]

I searched for all comparisons where the left and right hand sides have different types.

If we exclude cases where either side is a constant (e.g., inlen > 0 corresponds to size_t > int), then there are only six results.

Five results occur in fips202.c and fips202x4.c, and all of them involve upcasting r from unsigned int to size_t. So this can never result in an issue, even when verification is turned off.

The sixth result occurs in verify.h, where the comparison i < len corresponds to unsigned int < size_t. I am suggesting to avoid this mismatched comparison by declaring i as size_t instead of unsigned.

This is not a bug, but a potential issue if mlk_ct_memcmp is used to replace memcmp in an unrelated project where verification is turned off (otherwise the precondition on len will detect any issues).

I am suggesting my proposed change not as a bug but as a code improvement, as it may benefit projects that reuse mlk_ct_memcmp without verification.

[hanno-becker]

I think it's a good idea to flag comparisons with mismatched type, but I'm not convinced we have to make all types equal at the point of declaration. Instead, it seems to me that in a comparison with different types, one should down-cast the larger type to the smaller explicitly -- this would a) trigger CBMC to check that the cast is safe, b) require -- although we don't have a mechanical way to enforce this yet -- some // Safety: ... prose.

[nmouha]

Thank you, @hanno-becker, for your reply! I really appreciate your thoughts.

If i < len is replaced by i < (unsigned) len, then the issue that mlk_ct_memcmp behaves differently from the standard C library's memcmp still remains (for values of len that don't match the precondition, so not relevant for mlkem-native).

This is only an issue if mlk_ct_memcmp is reused in a project that doesn't use CBMC (otherwise len is checked).

So this is not a bug in mlkem-native, but arguably an enhancement to make mlk_ct_memcmp more reusable.

[rod-chapman]

Switching to size_t here makes the proof blow up with Bitwuzla. If you strengthen the loop invariant to maintain the fact that i <= UINT16_MAX and switch to use Z3 for the proof, it completes OK in about 40 seconds.

[rod-chapman]

Alternatively, you can leave unsigned i; alone and change the formal parameter to const unsigned len (which is fine given the pre-condition that len <= UINT16_MAX). This removes the mis-matched comparison, and the proof is almost instant with Bitwuzla.

[nmouha]

Thank you, @rod-chapman, for chiming in! I really appreciate your insights.

I just made some changes as I'm trying to build a stronger case for my PR.

• proofs/cbmc/proof_guide.md states: "mlk_ct_memcmp() shows that, functionally, it is just an ordinary memcmp()." However, if we relax the precondition on len, the CMBC proof with unsigned i instead of size_t i will fail.
• mlkem/src/verify.h states: len is "upper-bounded to UINT16_MAX to control proof complexity only." However, the problem is not with the proof complexity, but with the formulation of forall in mlkem/src/cbmc.h (the backwards implication <== doesn't hold unless the forall is over all indices).

So, I'm proposing not just to change unsigned i by size_t i, but also to relax the precondition on len to show a CBMC failure without this change.

@hanno-becker, @rod-chapman: Looking forward to your thoughts!

[rod-chapman]

I fear this will blow up proof times. We have tried this before and found that quantifying over size_t instead of unsigned resulted in an SMT encoding where quantification occurs over 64-bit bit-vectors. This has a rather poor impact on proof times with Z3.

[nmouha]

You are right that there is an increase in proof times, but maybe it's still reasonable.

Currently, the ct_memcmp proof is generated by Bitwuzla, not z3.

My PR increases the proof time on my laptop from 0.5 seconds to 2 seconds (for one SMT2 input).

[nmouha]

Seems the proof time is halved when using cvc5 instead of Bitwuzla (from two seconds to one second).

So, I've changed the Makefile to use cvc5 instead.

[rod-chapman]

1. My concern is that changing cbmc.h will impact all the proofs.
2. We don't currently use cvc5, and it is not built or installed by our NIX config.

[nmouha]

Thank you, @rod-chapman, for clarifying! I see that I had some tunnel vision as I was focusing only on mlk_ct_memcmp. Moreover, cvc5 was already part of my environment.systemPackages, so I didn't notice that Nix support was incomplete.

Anyway, you're completely right that my proposed change to cbmc.h impacts many proofs, and that several of them result in timeouts.

I'm proposing to solve two problems at once: complete cvc5 support (cvc5 is already in the Proof Guide and Makefile, just the Nix package is missing), and use cvc5 to avoid the timeouts.

Looking forward to your thoughts!

[rod-chapman]

What versions of cbmc and cvc5 are you using? None of these changes work for me.
I am als unsure of taking a dependency on cvc5 (and adding to our TCB and Soundness case), all for the sake of a 1-line cosmetic change.

[hanno-becker]

I fear this will blow up proof times. We have tried this before and found that quantifying over size_t instead of unsigned resulted in an SMT encoding where quantification occurs over 64-bit bit-vectors. This has a rather poor impact on proof times with Z3.

I agree with that. This is an area that we have explored extensively, and found to be proof-time sensitive. Apart from the inconvenience of waiting for a PR to pass CI, the CBMC proofs also incur a meaningful CI cost -- we don't want to increase that unnecessarily.

My stance from the original reply remains: I think it is good to flag those comparisons and potentially add a CodeQL (or similar) query to check for them, but I think the resolution should be an explicit down-cast at the time of comparison, which is then subject to the usual safety checks. That mld_ct_memcmp differs from a normal memcmp in signature is not an issue I think -- perhaps rather a feature, because those really ought not to be conflated.

But, bottomline is still, I'm grateful you brought this up, and I think this is worth our awareness. But I don't think it justifies global changes such as changing the CBMC configuration.

[nmouha]

Thank you, @rod-chapman and @hanno-becker, for sharing your thoughts.

I want to clarify that these changes are not cosmetic: they fix an error in mlkem-native's forall/exists macros. Currently, forall(i, 0, len, P(i)) does not quantify over all i in [0, len), because i is unsigned instead of size_t (so 32 bits instead of 64 bits on 64-bit platforms). This means proofs that rely on forall are unsound for values of len beyond what CBMC happened to explore.

Concretely, here is an incorrect mlk_ct_cmov_zero that passes the current CI:

size_t i;
for (i = 0; i < len; i++)
__loop__(
  invariant(i <= len)
  invariant(forall(k, 0, i, r[k] == (b == 0 ? x[k] : loop_entry(r)[k])))
  decreases(len - i))
{
  r[i] = mlk_ct_sel_uint8(r[i], x[i], b);
  if ((b != 0) && (i == (1ull<<32))) {
    r[i] ^= 1; // bug: corrupts at i == 2^32
  }
}

My PR fixes forall so that it actually quantifies over all indices, detecting these types of bugs. No bugs are found in mlkem-native itself, but the proofs are now sound.

Regarding proof times: on the main branch I already see timeouts for mlk_indcpa_enc, mlk_keccak_squeeze_once, and poly_ntt_native on my laptop (using the Nix environment). The solver switch avoids these pre-existing timeouts for me. Therefore, I expect that #1691 (full CI) on my updated PR will show reduced solver times as well.

On the TCB concern: does the current CI validate unsat cores for Z3 or Bitwuzla proofs? If not, then adding cvc5 doesn't change the trust model: unsound solver bugs are undetected either way. If solver diversity is the concern, adding a third solver actually improves confidence by reducing dependence on any single SMT solver implementation.

On the len bound: the comment in verify.h says UINT16_MAX is "to control proof complexity only," but Bitwuzla proves correctness without this bound in ~2 seconds, so that justification doesn't hold.

I'd be grateful if you'd consider running the full CI to check that the proof-time concerns are manageable, and consider correcting fixing the error in the forall/exists macros to ensure that the proofs are sound.

[hanno-becker]

@nmouha Thanks for persisting and for clarifying that you suspect a soundness issue, which is obviously much more serious.

I ran your example:

static MLK_INLINE void mlk_ct_cmov_zero(uint8_t *r, const uint8_t *x,
                                        size_t len, uint8_t b)
__contract__(
  requires(len <= MLK_MAX_BUFFER_SIZE)
  requires(memory_no_alias(r, len))
  requires(memory_no_alias(x, len))
  assigns(memory_slice(r, len))
  ensures(forall(i, 0, len, (r[i] == (b == 0 ? x[i] : old(r)[i])))))
{
  size_t i;
  for (i = 0; i < len; i++)
  __loop__(
    invariant(i <= len)
    invariant(forall(k, 0, i, r[k] == (b == 0 ? x[k] : loop_entry(r)[k])))
    decreases(len - i))
  {
    r[i] = mlk_ct_sel_uint8(r[i], x[i], b);
    if (i == (1ull<<32)) {
	r[i] ^= 1; // bug: corrupts at i == 2^16
    }
  }
}

And I confirm that it passes CBMC.

As I understand it, the issue here is not with CBMC but with our wrapper around forall. Our model of forall asks CBMC to show that the post-condition is true for all i up to UINT32_MAX, and that's indeed the case -- the bug manifests only beyond. But still it's highly misleading, because clearly everybody would read forall(i, 0, len, ...) as a quantification up to the full len.

In the case of mlkem-native, the distinction doesn't really matter because we don't deal with buffers beyond UINT32_MAX size, and that's why we allowed ourselves the lower bound for performance reasons.

We need to improve this. We either remove the restricted scope of forall, or we must make it explicit. Two options:

• We widen the quantifier to size_t and find a way to deal with the performance and cost ramifications.
• We document the limits of forall and enforce them by explicitly truncating LB and UB to unsigned. If we ever pass a bound where CBMC cannot prove that it fits within unsigned, it will fail -- including the example above. This is in line with the linting I suggested where we demand that all unequal-type comparisons must use down-cast of the larger type. And then we need to accordingly bound the sizes of buffers in functions dealing with arbitrary lengths.

I am slightly leaning towards the second option because it avoids us fighting with runtime issues while still forcing us to make the limitations of the current forall(...) definition explicit (e.g. by putting requires(len <= UINT32_MAX) in the pre-condition of mlk_ct_cmov_zero above). But happy about opinions @nmouha @mkannwischer @rod-chapman

Thank you @nmouha again for flagging this -- I appreciate your detailed analysis and tenacity! 🙏

[hanno-becker]

@mkannwischer correctly points out the the option 2 is not ideal for mldsa-native, as a buffer size limit of UINT32_MAX (~4G) would be of practical relevance, albeit rare.

[nmouha]

Thank you, @hanno-becker! I appreciate your detailed reply.

I would like to reiterate my proposed PR not only uses size_t in the quantifier, but I made some solver switches to avoid pre-existing timeouts that I was experiencing on my laptop. So, performance should be improved compared to the main branch.

Maybe running a full CI on my PR can alleviate your performance concerns?

[nmouha]

Oh, I see just now that you've started running a full CI on my PR already in #1695. Looking forward to the results!

[hanno-becker]

@nmouha Yes unfortunately we still need to start a PR from the main repo for full CI...

[hanno-becker]

@rod-chapman Do you have data regarding stability and trustworthiness of CVC5?

[hanno-becker]

Closed automatically but unintentionally by the merge of #1694. Reopen.