The description on that page makes some great points for me. Firstly, and I think most importantly
At each stage in the process verification activities were undertaken to ensure that no errors had been introduced. These activities included review and semi-formal verification techniques applicable to the entities being developed.
In other words: “we can’t actually apply formal methods to the entire process, so we did some ad hoc stuff, too”. Core to this problem is that you have to somehow describe what it is you are trying to do. In order to disguise the problem, formal methods folk like to call this a specification – but when you get down to it, it’s a program. Which can have bugs in it. Which you can only diagnose by thinking about it and testing.
Next, from the overview, section 5
Since release 7.4, SPARK has included an “accept” annotation that can be used to justify expected warnings and errors. These annotations have been added as appropriate.
In other words, verification fails, but these failures are “justified”. Hmmm.
Again from the overview (section 5.3) even after formal verification a bug was found, which was an elementary integer overflow bug. I would hope any competent programmer would have spotted this as they were writing the code, but apparently it was beyond all this expensive and painful infrastructure.
Finally (there’s more, but I have other things to write about, so I’ll stop here), again from the summary
# lines of code: 9939
# total effort (days): 260
Wow. That’s a lot of days for not very much code.
Toby asked “how would you feel about a proposal that asked for a range of standard software modules whose design had been subjected to formal analysis, at some semi-useful and reasonable level of abstraction, of some of its key functional/security properties?”
I guess I feel about this rather as Gandhi felt about Western civilisation: it would be a good idea.
More positively, I imagine there are actually some modules that are sufficiently small in scope that one could convince oneself that the specification was actually correct, and maybe even prove that the implementation matched the specification. For example, things like arrays, sets and maps might be implementable correctly. Where it all falls apart, in my view, is when you try to make a system that actually does something useful: then you get into the realm where debugging the specification is the hard problem.
I think this actually might be achievable, and perhaps even desirable. But I’m not so sure it would be truly useful. A microkernel architecture inherently punts on all the interesting security questions and simply enforces whatever incorrect decisions you have made outside the kernel. So, you are still left with all the real-world security problems, but at least you have a place to stand when you claim you are enforcing whatever security properties you think your code implements (that is, you can discount the microkernel as a source of problems and only have to worry about the other 99% of the code).
I also strongly suspect that a team of skilled engineers could carefully write a secure microkernel that was just as robust without any need for formal verification. More quickly and with less swearing.
This is a great point, and I actually agree. I’m a big fan of type safety, as anyone who’s seen some of the hoops I jumped through in both the Apache module system and more recently in OpenSSL will know. I really like things to break at compile-time rather than run-time if at all possible, and type safety is one way to achieve this (this is one reason I prefer C++ to C, despite its many defects). I guess functional languages also have interesting properties from that point of view but I feel like I understand them less. I really must learn Erlang (or Haskell, I suppose, but I’ve tried and failed a few times already – it seems there are no good tutorials out there).
Anil also says “Even for C, static analysis is increasingly used to track down bugs (with products like Coverity which are very effective these days)”.
Sorry, but no. I thought for quite a while that there was a future in static analysis. But the more I am exposed to it, the less I think it is true. The false positive rate is still fantastically high, even in Coverity, which is probably the best system I’ve played with, and even correct hits tend to be on the “academically correct but not actually useful” side.
I do continue to suspect that static analysis combined with annotation might be useful, though (e.g. as in Deputy). But really, this is just trying to bolt on strong typing to weakly typed languages and isn’t truly static analysis is we hoped it might be.
Finally, he says “If things continue like they have been, then weâ€™ll continue to cherry pick the practical developments from the formal methods community into mainstream languages, and reap the benefits.”
I certainly hope so, and I don’t want to discourage further research into formal methods. I just object to the notion that they are practical to the extent that we should be trying to use them wholesale to build real systems. They really aren’t.
I was intending to also talk a bit about things I think actually are useful for security, but I think I’ll leave that for a later post.