4 ms·
> there was no point in time that formally verified software was mainstream. Even attempts at that have turned out broken later on (e.g. KRACK attack on wpa2)
by staunton 3y ago
> there was no point in time that formally verified software was mainstream. Even attempts at that have turned out broken later on (e.g. KRACK attack on wpa2)
In what ways was wpa2 an attempt at formally verified software? The KRACK attack exploited an issue in the standard itself. Were notable implementations of it formally verified? Was the spec itself verified in some flawed ways? I read the Wikipedia page and couldn't find anything relevant.
- bawolff 3y agoSee section 6.4 of https://papers.mathyvanhoef.com/ccs2017.pdf https://papers.mathyvanhoef.com/ccs2017.pdf Essentially the spec was formally verified, but it turned out that the formal definition of "secure" they used wasn't sufficient. Formal verification only works if you properly define all the security relavent properties that need to be proven, and the process of defining them can have errors itself.