Missing reduction in negation in the base field

[pornin]

In the FieldElement56::negate() function: https://github.com/crate-crypto/Ed448-Goldilocks/blob/30946a3dcba264102a6812946f7fcacbcbd65f22/src/field/fiat_u64/prime_field.rs#L163-L168 the negation uses fiat_p448_opp(), but there is no fiat_p448_carry() (or its wrapper FieldElement56::strong_reduce()). In the fiat-crypto terminology, fiat_p448_opp() expects the input to be "tight" (limb values in the 0 to 2^56 range, inclusive), but outputs a value which is "loose" (limb values may go up to 3*2^56 in the loose range). Some other functions (e.g. addition, subtraction, and encoding) expect inputs to be tight, and the general rule of FieldElement56 is that it should contain loose values only transiently.

In practice, this means that the following test code would fail:

#[test]
fn test_negate() {
    let x = FieldElement56::zero();
    let y = x.negate();
    assert_eq!(y.to_bytes(), [0u8; 56]);
}

This code encodes the value zero (negated, but minus zero is still zero), and the only valid, canonical encoding of zero is a sequence of 56 bytes of value zero. Instead, what we get here from y.to_bytes() is the little-endian encoding of the field modulus. The reason is that "minus zero" yields a (loose) representation of 2*p (with p = modulus), and to_bytes() calls fiat_p448_to_bytes() which performs a single conditional subtraction of the modulus.

As far as I can tell, this is the only incorrect computation that follows from the lack of reduction post-negation, because the fiat-crypto routines from p448_solinas_64 accept, in fact, values which a much larger range than the formally proven ranges. Thus, as long as there is some arithmetic operation between any negate() and to_bytes() calls, the output should still be correct; this appears to be the case within the Ed448-Goldilocks crate. The issue, though, still gets out of the formal proof of correctness of fiat-crypto. My manual analysis indicates that there is no exploitable security issue (i.e. there is no way, through the public API, to make the library compute "wrong"), but manual analysis is not as good as a formal proof, which was the point of fiat-crypto.

The fix is easy: add a result.strong_reduce() call just after the call to fiat_p448_opp().

[kevaundray]

Thanks for the detailed write-up and the suggested fix!