Secure Coding mailing list archives
Cost of provably-correct code
From: crispin at novell.com (Crispin Cowan)
Date: Sun, 23 Jul 2006 20:59:42 -0700
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 2L 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
Current thread:
- bumper sticker slogan for secure software, (continued)
- bumper sticker slogan for secure software Pascal Meunier (Jul 20)
- bumper sticker slogan for secure software der Mouse (Jul 20)
- bumper sticker slogan for secure software ljknews (Jul 20)
- bumper sticker slogan for secure software John Wilander (Jul 21)
- bumper sticker slogan for secure software Crispin Cowan (Jul 21)
- Cost of provably-correct code (was: bumper sticker slogan for secure software) David Crocker (Jul 21)
- Cost of provably-correct code (was: bumper sticker slogan for secure software) der Mouse (Jul 22)
- Cost of provably-correct code Crispin Cowan (Jul 23)
- bumper sticker slogan for secure software mikeiscool (Jul 23)
- security half-life and critical mass securecoding2dave at davearonson.com (Jul 21)