mirror of
https://github.com/wolfSSL/wolfssl.git
synced 2026-08-11 06:21:19 +02:00
Daniele Lacamera
a17cc4ee4e
Premise: ed448.c:1511 `if ((ret == 0) && ed448_is_small_order(key->p)) {
...; ret = PUBLIC_KEY_E; }`, and ed448_is_small_order (:245-312),
which zeroes byte 56 of a copy of the input and memcmps it against a
table that explicitly includes the non-canonical y = p encoding
(:283-291: 0xff x28, 0xfe, 0xff x27, 0x00).
Claim: ed448.c:1554 `if ((ret == PUBLIC_KEY_E) && (key->p[0] < 0xff))` --
the `key->p[0] < 0xff` operand, whose false half is the Y == p case.
Proof: reaching :1554 requires the preceding range walk to have found
p[56..29] all 0xff (loop at :1533), p[28] == 0xfe (:1543) and
p[27..1] all 0xff (loop at :1546). If p[0] were also 0xff the input
would be exactly the y = p encoding modulo byte 56 -- which
ed448_is_small_order masks -- so :1511 would have set
ret = PUBLIC_KEY_E and the else-if arm containing :1554 would never
have been entered. The operand can only ever evaluate true, so its
independence pair is unreachable.
With that operand fixed true, the remaining `ret == PUBLIC_KEY_E`
operand no longer decides anything: when it is false the bottom loop
has already set ret = 0. Both paths end with ret == 0, so the whole
conditional collapses to `ret = 0;`.
Scope: neither wc_ed448_check_key nor ed448_is_small_order is conditionally
compiled, so this holds in every configuration that builds ed448.c.
Evidence: llvm-cov MC/DC records no covered pair for this condition in any
ed448 variant.
Rejection semantics are unchanged: y = p is still refused, by
ed448_is_small_order rather than by this byte walk, and every other encoding
takes the same path as before. The table's y = p row is therefore what enforces
the upper end of the Y range; ed448_is_small_order carries a note saying so, so
the dependency is stated where the invariant is produced as well as where it is
consumed.
ed448.c is inside the FIPS module boundary. Released FIPS flavours pin ed448.c
to a tag and are unaffected; fips-dev/fips-ready build from master and
recompute the in-core hash.
With the last-byte test gone, the loop over p[27..1] can no longer affect the
outcome -- its only effects were setting ret = 0 and breaking -- so it goes too,
and the two surviving arms both yield ret = 0, collapsing to a single
`p[ED448_PUB_KEY_SIZE/2] <= 0xfe` test. The only input for which this differs
from the original is exactly the y == p encoding, which the proof below shows
never reaches here.
Proof check: gcc does not fold this (it cannot reason about the small-order
table). Machine-checked exhaustively instead: the byte walk pins 56 of the 57
public-key bytes before the final test, leaving p[0] as the only free variable,
so all 256 values were enumerated against the real ed448_is_small_order(). Two
values (p[0] = 0xff, y = p; and p[0] = 0xfe, y = p-1) are rejected early by the
table; the other 254 reach the final test and all satisfy p[0] < 0xff. Zero
counterexamples over the complete state space.
Also checked with clang's deadcode.DeadStores analyzer (the checker behind the
clang-tidy CI legs): clean on this file, with the two pre-existing sp_int.c
core.* findings unchanged from master.