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]
