Cost of provably-correct code

[crispin at novell.com (Crispin Cowan)]

David Crocker wrote:
> 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
> L 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.
I did not arrive at it. It is (allegedly) the NSA's estimate of cost per
LOC for EAL7 provably correct assurance. This was quoted to me from a
friend at a company who has an A1 (orange book) secure microkernel.

> >  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.

Interesting. That could possibly bring down the cost of High Assurance
software enormously.

How would your prover work on (say) something like the Xen hypervisor?
Or the L4 microkernel?

Caveat: they are C code :(

Crispin

-- 
Crispin Cowan, Ph.D.                      http://crispincowan.com/~crispin/
Director of Software Engineering, Novell  http://novell.com
     Hack: adroit engineering solution to an unanticipated problem
     Hacker: one who is adroit at pounding round pegs into square holes