Learn from CBMC specification bug #985

[hanno-becker]

• Relates to: CBMC: Correct operator precedence in ensures clause of mld_caddq() #985

Bug #985 concerned a wrong CBMC specification stemming from misinterpreted operator precedence. Luckily, the issue was 'benign' insofar that the affected post-condition was not relevant for type-safety, but it is nonetheless a cautionary tail.

Task:

• Consider what, if anything, could have been done in CI to catch this.
• Explicitly point out which SOUNDNESS.md risk this bug falls under; and if there's no suitable risk, add one.

[tautschnig]

Is this function call from anywhere? If so, mlkem-native's SOUNDNESS.md (there isn't one for mldsa-native, is there?) covers this in https://github.com/pq-code-package/mlkem-native/blob/9aa410b51953dd340c2813c81b1b27fbfd2e123c/SOUNDNESS.md?plain=1#L234.

[mkannwischer]

Is this function call from anywhere? If so, mlkem-native's SOUNDNESS.md (there isn't one for mldsa-native, is there?) covers this in https://github.com/pq-code-package/mlkem-native/blob/9aa410b51953dd340c2813c81b1b27fbfd2e123c/SOUNDNESS.md?plain=1#L234.

Yes, caddq is called from poly_caddq, but the post-condition in question ensures(return_value == ((a >= 0) ? a : (a + MLDSA_Q))) (which models correctness of caddq) is not required to prove the post-condition of poly_caddq - for that we only need the other two post-conditions of caddq (ensures(return_value >= 0) and ensures(return_value < MLDSA_Q) which model the output bounds).

This is a case where we wanted to model a stronger spec for a leaf function because it is feasible, but ended up modelling something that is not proving anything.

I wonder if there is any way to make CBMC warn about ensures((return_value == (a >= 0)) ? a : (a + MLDSA_Q))? I think it is even happy with ensures(return_value). If we could somehow make it fail on non-boolean types, we could eliminate this class of problems.

[tautschnig]

I wonder if there is any way to make CBMC warn about ensures((return_value == (a >= 0)) ? a : (a + MLDSA_Q))? I think it is even happy with ensures(return_value). If we could somehow make it fail on non-boolean types, we could eliminate this class of problems.

CBMC is good a precisely modelling C semantics, even when the input may be somewhat awkward. In my opinion you are looking for a linter, and while we could re-use CBMC's C front-end to facilitate that I'd guess that even directly using an LLM will give you better results: it would be way more flexible for a variety of rules can simply be expressed in natural language.