Hi,
> Op 8 jul 2026, om 09:46 heeft Stephan Neuhaus <[email protected]> het volgende
> geschreven:
>
> On the toolchain side, I am not aware that gcc or LLVM (for example) have
> formal correctness proofs. And even if those existed, we have seen with
> KyberSlash that the concrete choice of instruction, while strictly preserving
> the "observable behaviour" of a program (which is what a C compiler cares
> about) can introduce side channels.
Compiler-introduced side channels exist and are fairly common for EC and
RSA-based implementations as well. Serious implementations of crypto, PQ or
not, tend to be written in assembly to avoid toolchains (though CPUs themselves
are also a hazard!).
Additionally, we have a fairly rich set of (to varying degrees) formally
verified implementations of ML-KEM (including, but not limited to, libcrux,
mlkem-native, mlkem-libjade). Many of them include side-channel resistance to
varying degrees as one of the verification goals; libjade even targets
transient execution (SPECTRE).
Regards,
Thom Wiggers
_______________________________________________
TLS mailing list -- [email protected]
To unsubscribe send an email to [email protected]
