3 ms·
Formal verification is not the same as a security audit. With formal verification you can prove that something is bug-free. > They find issues in libCURL and o
by snakeanus 9y ago
Formal verification is not the same as a security audit. With formal verification you can prove that something is bug-free.
> They find issues in libCURL and openSSL that have existed for years
Neither of them are formally verified. https://github.com/seL4/seL4 https://github.com/seL4/seL4 however is formally verified.
- sqeaky 9y agoPlease, step away from "formal verification" and come back to world the rest of us devs work in. I have never seen a formally verified piece of software even once. I don't know if its too hard to do to real software or if C doesn't allow for it, or if it is just too expensive. The simple matter is that is not an option for the vast majority of projects. Unless you can make it practical, I assert it has no place in a practical discussion about preventing software issues.
- AnimalMuppet 9y agoWorse: "It's amazing how many bugs there can be in a formally verified piece of software." I forget who said it, but it's been a long time. (Maybe in connection with formal verification of an OS? Does anyone remember?) Formal verification only works if the formal verification was mistake-free. (And how are you going to prove that? With a formal verification? It's turtles all the way down...) Also, it only works for the aspects that were formally verified. Heartbleed, for example, could be regarded as a flaw in the specification; formally verifying that the code matches the spec won't save you from that.