[TLS] Re: WG Last Call: draft-ietf-tls-mlkem-08 (Ends 20 26-07-08)

On 7/7/26 7:00 PM, Tanja Lange wrote:
 > This might be one part of the misunderstanding. There are (at least) 
3 layers
 > where formal verification is needed
 > * protocol level,
 > * proof of primitives level,
 > * implementation level.

I think you're right with the "at least": Assuming that "implementation 
level" means "source code level", one might add at least two more:

* toolchain level
* platform level

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.

Cheers

Stephan

_______________________________________________
TLS mailing list -- [email protected]
To unsubscribe send an email to [email protected]