Rick Smith <smith @
com> replied to Marcus Ranum: (portions deleted)
>If there's anything "wrong" with formal assurance it's the simple fact
>that it's easy for careless practitioners to do it wrong, and expend a
>mjr> system meets its requirements. Big Deal -- you're not able to
>mjr> *prove* that the system actually *works* as specified, though
>mjr> you can use this process to obtain a massive body of evidence
>mjr> that points to its working the way you hope it does.
>Without the formal proofs, you have nothing but "hand waving" to
>show that your security requirements are fulfilled by your design.
This thread seems valuable to the need to make business decisions on choosing firewalls. Determining "how much" firewall (or other protection) is an important but non-trivial consideration. We need better tools to support those decisions.
Software is notoriously difficult to verify. Some folks are trying the process models like that of Watts Humphry ("CMM"). Some are looking at applying the traditional risk management tools. The current alternatives seem to be misleading rigor or wing-
and-prayer hopefulness. We need something in between. Perhaps this group can come up with something.
I recall a story about Dennis Ritchie or someone of his stature presenting a challenge to find the backdoor in a couple hundred lines of code. The challengees came back in a tizzy declaring the challenger had hoaxed them with clean code. They were shown
not one but TWO security breaches, one that he though was a "gimmee" which would throw them off the better one.
Moral - it's not practical to assure any software these days. But we still need effective decision support techniques.
Trident Data Systems, LA