Proving security protocols

[Rick Smith at Secure Computing]

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.
smith at securecomputing.com            roseville, minnesota
"Authentication" in bookstores http://www.visi.com/crypto/




---------------------------------------------------------------------
The Cryptography Mailing List
Unsubscribe by sending "unsubscribe cryptography" to majordomo at wasabisystems.com