At 09:00 AM 11/1/2001, Roop Mukherjee wrote: >Can someone offer some criticism of the practice formal verification in >general ?
Okay, I'll grab this hot potato. There are a few cases where a commercial development organization performs formal verification, which would seem to indicate that it can in fact provide benefits that outweigh the costs. In particular, I know that DEC/Compaq and Motorola have used formal verification, at least to some degree, to detect flaws in integrated circuit designs. This makes sense because it's so expensive to recover from an IC design flaw, so it's cheaper to spend money up front on eliminating possible flaws. If you're building your crypto protocols into hardware, particularly silicon, then you might see similar benefits to formal protocol assurance. On the other hand, the software industry has marketed itself into a situation in which vendors are penalized if they spend too much effort on quality assurance, whether it be formal methods or even just testing. I've heard that NSA put a lot of effort into crypto protocol verification, but they weren't constrained by the same economic forces as others. A colleague who does formal verification of ICs looked at formal verification of non-crypto networking protocols a few years back, and concluded that the developers achieved sufficient quality through conventional testing. The most recent issue of ACM's Transactions on Info Security carries my article on LOCK TCB assurance costs, and I made a number of observations on the cost/benefit of formal assurance in secure OS development. There's no either/or regarding testing and formal assurance: the question is whether you can afford to take money from your testing budget to pay for formal assurance. Bottom line: the LOCK experience suggests that you find more flaws through testing (per unit of resources spent) than you find through formal assurance. You can generally find a way to test (or at least exercise) just about every requirement and capability in a typical software product, but formal assurance can't come anywhere close to that degree of coverage in real world systems. Testing might not detect all flaws, but neither will formal assurance. Ultimately, the decision to use formal assurance is driven by the types of flaws you need to detect, and the risks to the product caused by such flaws. In LOCK, there was a huge desire to detect covert channels before the system was deployed, and the assurance effort was deemed to be successful at pursuing that goal. Rick. [EMAIL PROTECTED] roseville, minnesota "Authentication" in bookstores http://www.visi.com/crypto/ --------------------------------------------------------------------- The Cryptography Mailing List Unsubscribe by sending "unsubscribe cryptography" to [EMAIL PROTECTED]
