While not disagreeing with anything Paul wrote, I wanted to make some comments about the state of formal verification technology.
Quoting [EMAIL PROTECTED]: > 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 _______________________________________________ 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 SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com) as a free, non-commercial service to the software security community. _______________________________________________
