3 ms·
> how did this attack slip through, despite the fact that the 802.11i handshake was formally proven secure? So, we cannot trust even formal verification? > it
by progman 9y ago
> how did this attack slip through, despite the fact that the 802.11i handshake was formally proven secure?
So, we cannot trust even formal verification?
> it’s a factual statement. In formal analysis, definitions really, really matter!
If lack of definition implies flaws in formal verification, does that mean we need an additional formal verification of formal verification?
Update:
> We need machine-assisted verification of protocols, preferably tied to the actual source code that implements them.
Haskell, here is your opportunity :-)
- twinkletwinkle 9y agoFormal verification all the way down. I'm a complete layman in this field, but mustn't it bump against the Incompleteness Theorem at some point? There's no way to prove your definitions.
- progman 9y agoThe critical point is specification vs. implementation. Any difference creates a loophole which can be abused.
- ecesena 9y ago> So, we cannot trust even formal verification? it's explained in the article, 2 unit tests, 0 integration tests. The formal verification appears to prove correctness of the 2 pieces independently, but not of the composition. > Haskell, here is your opportunity :-) you're just moving the problem to the correctness of the compiler.
- petters 9y ago> you're just moving the problem to the correctness of the compiler But it would be a huge leap forward.