3 ms·
Even 100% formally verified code could be vulnerable to side channel and other hardware attacks. There could also be bugs in the verification system, the compi
by empath75 7y ago
Even 100% formally verified code could be vulnerable to side channel and other hardware attacks. There could also be bugs in the verification system, the compiler, the spec that they’re verifying, nothing is hacker-proof.
- not2b 7y agoYes, a formal proof shows that a system does not have a specified class of bugs, subject to specific assumptions. This is very valuable, but it is better to think of it as another (very powerful) bug finding technology than a complete assurance that nothing can go wrong.
- aliceryhl 7y agoYou might not ever reach 100% confidence, but formally verified code is a whole lot more likely to be correct than code that is not formally verified.