Software verification and software engineering a practitioner's perspective

Abstract

The web page for this conference announces a "Grand Challenge" of crucial relevance to society: ensuring that the software of the future will be error-free. According to the Scope and Objectives In the end, the conference should work towards the achievement of the long-standing challenge of the Verifying Compiler. I want to question whether this long-standing challenge is really relevant to the greater goal of achieving trustworthy software. Instead, I suggest that research in verification needs to support a larger effort to improve the software engineering process. I am a strong advocate - And a practitioner - of formal methods as part of a rigorous software engineering process. But formal methods are very much more than program verification. The goal of verification is to take a given program and to prove that it is correct. The goal of software engineering is quite different: it is to create a program that is verifiably correct. Program verification is neither necessary nor sufficient for software engineering. Its pursuit may even have harmful consequences. To illustrate, let me take two examples from the field of security. First, consider the appalling fact that most security flaws are caused by buffer overflow. Why is this appalling? Because there is absolutely no need for anyone, ever, to write a program that contains buffer overflows. That we continue to do so is a reflection our addiction to atrocious languages like C++. There are perfectly good languages around that make it simply impossible to write code that can cause buffer overflows. We should use them. No research is necessary. No proofs are necessary. It's a decidable - indeed solved - problem. Now let me take a more sophisticated example: cryptography on smart cards. This is a field that seems to be natural for verification. Indeed we could hope to prove, for example, that a cryptographic algorithm needed exponential time to break by brute force and that it was correctly implemented on a smart card. So the smart card would be secure, right? Wrong. Along comes Paul Kocher with a watt meter and breaks the key that you have proved is secure. How did he do that? He did it by bypassing the assumptions you made in your proof. But you never even stated those assumptions: how many proofs contain the following assumption?. © IFIP International Federation for Information Processing 2008.