mirror of
https://github.com/wolfSSL/wolfssl.git
synced 2026-08-19 17:33:26 +02:00
Daniele Lacamera
d95bef3d39
Premise: wc_MlKemKey_EncodePublicKey ends with
if (ret == 0) { key->flags |= MLKEM_FLAG_H_SET; }
(wc_mlkem.c:2796-2799). It is the only definition of that function in
the tree and is unconditional inside WOLFSSL_HAVE_MLKEM.
Claim: wc_mlkem.c:1428-1431,
if ((ret == 0) && ((key->flags & MLKEM_FLAG_H_SET) == 0))
ret = BAD_STATE_E;
Proof: two cases at :1428.
(a) MLKEM_FLAG_H_SET was already set on entry: the block at :1398 is
skipped entirely and nothing clears the flag, so the second
operand is false.
(b) The flag was clear: reaching :1428 with ret == 0 requires
wc_MlKemKey_PublicKeySize to have succeeded, the (malloc build)
allocation to have succeeded, and wc_MlKemKey_EncodePublicKey to
have returned 0 -- which sets the flag. Again the second operand
is false.
{ret == 0, H unset} is therefore unreachable, the condition can never
be true, and BAD_STATE_E can never be returned from here.
Scope: both the WOLFSSL_NO_MALLOC and !WOLFSSL_NO_MALLOC arms of the block
funnel through the same EncodePublicKey call; the size-failure and
allocation-failure paths both leave ret != 0. The enclosing
!WOLFSSL_MLKEM_NO_ENCAPSULATE || !WOLFSSL_MLKEM_NO_DECAPSULATE gate
selects whether the function exists at all.
Evidence: llvm-cov MC/DC records both of this decision's conditions as
uncovered (reports/mlkem/GAPS.md rows 1373:9:1373:61:0 and :1, at the
pre-drift line numbers) -- they are the only two residuals holding
wc_mlkem.c at 66/68.
The comment called it an "implementation issue" check, i.e. an assertion
against a future encoder that forgets the flag; it is being removed rather than
retained because no call path can reach it.
Proof check: gcc does not fold this (the encoder call is not inlined).
Verified instead by enumerating every write to key->flags in the translation
unit -- all nine, at wc_mlkem.c:453, 621, 852, 1001, 1003, 2283, 2327, 2430 and
2794, living in Init, Free, MakeKeyWithRandom, DecodePrivateKey,
DecodePublicKey and EncodePublicKey. wc_mlkemkey_check_h calls only
wc_MlKemKey_PublicKeySize, XMALLOC, wc_MlKemKey_EncodePublicKey and XFREE, so
the sole flag write reachable from it is :2794, which SETS MLKEM_FLAG_H_SET on
ret == 0. No reachable path clears it.