3 ms·

> The problem involves so many dependencies that it is impossible for an individual and maybe even megacorporations to fully audit the code base and prove the s

> The problem involves so many dependencies that it is impossible for an individual and maybe even megacorporations to fully audit the code base and prove the software behaves as intended. Everything these days is best effort. Everything has always been best effort, 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) so its not a pancea. > We _need_ a native interface that portable software can target, to at LEAST get to the level where 'If you trust the OS, then the rest of the software is known to behave as expected' is a statement that can be made to have a plausibly secure environment for End to End Encryption on anything. This doesn't really make sense unless this portable interface contains the entire App. Like how do you imagine such a system would work? What would such an interface do or contain that would bring this dream even remotely close to reality?

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 ago
  See 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.

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 ago
See 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.