SC-L Digest, Vol 3, Issue 197

[dcrocker at eschertech.com (dcrocker at eschertech.com)]

While not disagreeing with anything Paul wrote, I wanted to make some  
comments about the state of formal verification technology.

Quoting karger at watson.ibm.com:

> The Orange Book explicitly wanted to include only requirements that
> had been shown to be feasible at the time the criteria were written (1985).
> At that point in time, formal verification of design specifications
> was clearly feasible (although difficult), but formal verification
> of sizable amounts of source code was clearly not yet feasible.  Even
> today (2007), formal verification of large amounts of source code is
> still very difficult.

In my view, as long as we are trying to verify handwritten code, it  
always will be very difficult. if formal verification is the goal,  
it's far better to refine specifications to code by adding design  
detail, using a mixture if manual and automatic methods. It's a real  
shame that people still spend so much time writing code in low-level  
programming languages like C and C++.

(snip)

> The Orange Book and the Common Criteria explicitly require penetration
> testing, particularly at the higher levels, as well as lots of other
> techniques.  This is because you can never assume that just a single
> security measure will solve all problems.  Even formal proofs can have
> bugs.  High assurance uses formal methods and testing and penetration and
> development procedures, etc. as a combination of methods is much less
> likely to leave latent problems that relying only on a single method.
> I don't think that security testing will ever not be necessary, even
> with full code proofs.  Proof tools can have bugs and they only show
> corresponce to specifications.  Specifications can also have errors.

Bugs in formal proofs are less likely now than they were in 1985  
because formal proofs are now always generated using automatic or  
interactive theorem provers. This has been found to be more reliable  
than manual proof (as well as much faster). The real problem is in  
getting the specification right. Some things come for free - for  
example, every system for producing verified code that I know of will  
provide a guarantee of no buffer overflow, assuming all the proofs  
have been done. However, in general it is very hard to specify "this  
system is secure" because we don't know all the ways in which it might  
not be secure, for example against classes of attach that haven't been  
discovered yet.

David