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 _______________________________________________ Secure Coding mailing list (SC-L) SC-L@securecoding.org List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l List charter available at - http://www.securecoding.org/list/charter.php
