Re:The Case for Formal Verification (2013)
by AnimalMuppet on Monday April 21, 2014 @01:23PM
(#7622277)
The article was talking about security. Security errors in specifications can be edge-case-like stuff. Or...
Back in the day, Microsoft very deliberately designed Outlook so that it could execute a file by having the user click on it. That was in the spec. It was also an enormous security hole. It wasn't just an edge case - the security hole was the essence of what the spec required.
If you get a spec like that, formal verification can do to things. It can tell you that yes, your code does what the spec says, without introducing any (additional) security bugs. That's somewhat useful, but it won't save you if the spec itself is the security bug.
Or, formal verification might be able to tell you that the spec itself is a security problem. That might not be called "verification", though - it might be called "theorem proving" or some such. It's in the same neighborhood, though.
Back in the day, Microsoft very deliberately designed Outlook so that it could execute a file by having the user click on it. That was in the spec. It was also an enormous security hole. It wasn't just an edge case - the security hole was the essence of what the spec required.
If you get a spec like that, formal verification can do to things. It can tell you that yes, your code does what the spec says, without introducing any (additional) security bugs. That's somewhat useful, but it won't save you if the spec itself is the security bug.
Or, formal verification might be able to tell you that the spec itself is a security problem. That might not be called "verification", though - it might be called "theorem proving" or some such. It's in the same neighborhood, though.