Cost of provably-correct code (was: bumper sticker slogan for secure software)

[dcrocker at eschertech.com (David Crocker)]

Crispin Cowan wrote on 21 July 2006 18:45:

> >
Yes, you can have provably correct code. Cost is approximately $20,000 per line
of code. That is what the "procedures" required for correct code cost. Oh, and
they are kind of super-linear, so one program of 200 lines costs more than 2
programs of 100 lines.
<<

To arrive at that cost, I can only assume that you are referring to a process in
which all the proofs are done by hand, as was attempted for a few projects in
the 1980s. We current achieve automatic proof rates of 98% to 100% (using PD),
and I hear that Praxis also achieves automatic proof rates well over 90% (using
Spark) these days. This has brought down the cost of producing provable code
enormously.

You are perhaps also including the cost of verifying the object code against the
source code. Although this is sometimes a requirement in the safety-critical
software world, I think it unlikely to be necessary for all but a very few
secure applications, assuming a mature compiler is used.

> >
Indeed, consider SQL injection attacks. They didn't exist 5 years ago, because
no one had thought of them. Same with XSS bugs. Same with printf format string
attacks. All of them are examples of processing user input without validation,
but they are all really big classes of such, and they were discovered to occur
in very large numbers in common code.

What Dana is trying to tell you is that some time in the next year or so,
someone is going to discover yet another of these major vulnerability classes
that no one has thought of before. At that point, a lot of code that was thought
to be reasonably secure suddenly is vulnerable.
<<

I agree, a new class of vulnerability may well be discovered. However, if the
code was specified and developed so as to be provably correct, then it is highly
likely that immunity to a new class of attack can be expressed by adding
additional formal requirements, allowing an immediate evaluation of where in the
design and implementation the vulnerabilities (if any) lie.

David Crocker, Escher Technologies Ltd.
Consultancy, contracting and tools for dependable software development
www.eschertech.com