[TLS] Re: WG Last Call: draft-ietf-tls-mlkem-08 (Ends 20 26-07-08)
Thom Wiggers <[email protected]>
| Newsgroups | gmane.ietf.tls |
|---|---|
| Message-ID | <[email protected]> |
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]