Cost of provably-correct code

[Ed.Reed at aesec.com (Ed Reed (Aesec))]

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

Well, not specifically for an EAL7 program, perhaps, but rather for a 
Class A1 system like ours, which is arguably a superset of an EAL7 
protection profile corresponding to the Mandatory Component (only) 
functional requirements for a Class A1 system under the Trusted Network 
Interpretation of the TCSEC.  That is, for a reference monitor 
verifiably enforcing the Mandatory Access Control (both integrity and 
secrecy) security policy (for Multi-Level Security), including formal 
top level specification and correspondence mapping to the 
implementation, including trusted distribution and RAMP (Ratings 
Assurance Maintenance Phase, which allows changes to the system to be 
evaluated incrementally rather than requiring re-examination of the 
whole system each time).

The system has a formally layered architecture (without loops) and can 
be configured with no covert storage channels (the only general purpose 
system we know of that can make such a claim),

Proving a software system is correct is one thing.  Proving it is 
correct as part of the hardware/software system of which it is a part is 
a second thing.  And proving you can securely deliver it and security 
revise it is yet something else, I suppose.

I expect that such a high cost estimate would include everything from 
clean-sheet design through evaluated configuration delivery of the 
product.  It's not the cost to prove something.  It's the cost to design 
and develop something you can prove, and then do so.
>   
> > > > >  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
The class A1 system referenced uses Pascal for the reference monitor / 
security kernel, with a small amount of assembler to handle 
hardware-interface things that couldn't be done any other way.

Pascal was chosen because it seemed a better fit than PL1, I 
suppose...for the 286-architecture environment for which it was 
originally developed.  It presently runs on Pentium-class processors.

A type-safe language was deemed necessary to support the assurance 
evaluation effort, as I understand it.

The formal internal model and top level specification is written in Ina 
Jo, the specification language of the Unisys Formal Development 
Methodology.  Reference section 7.6 "Design Specification and 
Verification" of the Final Evaluation Report for further details and 
section 8.18 "Design Specification and Verification" for the evaluators 
comments.  The Class A1 certificate is available at 
http://www.radium.ncsc.mil/tpep/epl/entries/CSC-EPL-94-008.html or our 
copy at http://www.aesec.com/eval/CSC-EPL-94-008.html (alas, the 
Evaluated Products List is no longer generally accessible, outside the 
.mil domain, at least - I'll be happy to provide a postscript or Acrobat 
PDF copy of the FER to anyone who asks me off line for it - please don't 
blast the list with such requests, though).

Ed
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://krvw.com/pipermail/sc-l/attachments/20060724/0721a432/attachment.html