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

Secure Coding mailing list (SC-L)
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php

Reply via email to