The case for formal verification of existing software

Perry E. Metzger takes a look at formal verification [removed dead link]. This is good stuff; there is a lot to agree with here.

However agreeing with Perry's post alone would not make a very interesting counterpoint. If agreeing was the only thing I intended to do I might even not have written this post. Instead I intended to add and I apologize in advance for the predictability of my views that while creating formally verified software from scratch is useful verifying existing software is useful too.

Yes formally verified software written from scratch can now be large enough in scope to be a compiler or a microkernel but when verifying existing software we can tackle the problem from the other end: we can pick any useful software component and verify that. We can pick a software component so useful that it is already used by millions. If we succeed in verifying it we have put formally verified software in the hands of millions of satisfied users. Transparently.

Take the example of the SSL implementation I am taking a couple of weeks to finish massaging through Frama-C. It is not as wide in scope as Quark seL4 or CompCert. Neither am I aiming for the same kind of functional correctness as these projects are: I am only verifying the absence of undefined behaviors in the component and verifying the functional dependencies of the cryptographic primitives(*).

But PolarSSL is useful. Plus by its very nature it is exposed to security attacks (SSL is the protocol behind HTTPS). And the former three examples are full-blown research projects in contrast to my single person.month effort.

The bonus is that the formally verified PolarSSL can be compiled and embedded with all the same compilers and into all the same firmwares as the earlier non-verified version. It is the same as the non-verified version except maybe for a couple of bugfixes and the confidence that for an identified usage pattern no more undefined behavior bugs will ever need to be fixed.

All in all the formal verification of existing code despite its differences from its “from scratch” counterpart has too become a force to be reckoned with.

(*) translation: I use Frama-C option -deps and I compare the result to what I expected

Acknowledgement: I got the link to Perry E. Metzger's post through Toby Murray.