Avoid mismatched comparison (suggested code improvement, not a bug!)

[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 five results.

Four 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 fifth result occurs in ct.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 mld_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 fix but as a code improvement, as it may benefit projects that reuse mld_ct_memcmp without verification.

[hanno-becker]

Hi @nmouha, Thank you for this! More than fixing the particular instance, I'd be interested in how to automatically detect this in the future. How did you find this? @mkannwischer and I were looking into using things like CodeQL or ast-grep for deeper code-analysis, but we haven't converged onto anything yet.

[hanno-becker]

(Same comment as in the other PR for mlkem-native) 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 the quick reply!

Of course I'm happy to explain how I found these instances. I did use CodeQL, here's my MismatchedComparisonTypes.ql:

/**
 * @name Comparison between different integer types
 * @description Detects comparison expressions where the left and right operands
 *              have different integer types (e.g., `unsigned int` vs `size_t`).
 *              A mismatch is allowed if one operand is a constant.
 * @kind problem
 * @problem.severity warning
 * @id mldsa-native/integer-comparison-type-mismatch
 * @tags correctness
 */

import cpp

from ComparisonOperation c
where
  exists(IntegralType lhs, IntegralType rhs |
    lhs = c.getLeftOperand().getType().getUnspecifiedType() and
    rhs = c.getRightOperand().getType().getUnspecifiedType() and
    lhs != rhs
  ) and
  not c.getLeftOperand().isConstant() and
  not c.getRightOperand().isConstant()
select c, "Comparison mixes types '" + c.getLeftOperand().getType().toString() +
         "' and '" + c.getRightOperand().getType().toString() + "'."

If you were considering to maybe use CodeQL, it's easy to enable it in GitHub and to add custom queries. I wrote about this here: https://mouha.be/sha-3-buffer-overflow-part-2/

However, I don't think there is an easy way to modify the CodeQL query to avoid the false positives in fips202.c and fips202x4.c...

If you are maybe considering a code change to avoid these false positives, then I'm suggesting size_t rsize = r; as the easiest fix.

[nmouha]

Converting this to draft due to the CI failures, sorry about that!

I will propose similar changes to mldsa-native once the PR for mlkem-native has converged: pq-code-package/mlkem-native#1690