Brian, >³Show me places in the program where property X holds²
Yes. That's it exactly. Current tools can answer this type of question to some extent, but they're not really designed for it. The interaction contemplated by most of the tools is more like "show me the line of code the vulnerability is on." This doesn't really help verify the security of an application and doesn't work at the design level. The "property X" approach does both. > aiding in program understanding, it needs to allow you to easily > add new rules of your own construction. This is absolutely critical. In addition to creating new rules, we need to be able to "tag" custom libraries and methods with their security properties. This will allow existing rules to be applied in new contexts. E.g. tagging a custom validation method with "untaint" so existing data validation rules now include it. > Whether or not you want to see this path depends on how important > it really is to you that encryption is absolutely never bypassed. > Your tolerance for noise is dictated by the level of assurance > you require. Absolutely. The encryption example demonstrates your point well. Still, I wouldn't want anyone to get the impression that there's a direct relationship between the signal-to-noise setting on the tool and the level of assurance one gets in an application. This is because the tools tend to find the problems that are easiest for them to find, not the ones that represent the biggest risk. For example, access control problems in web applications are difficult to find automatically, because the implementations are generally complex and distributed across a software baseline. So even if I only want a typical commercial level of assurance in a web application, I have to turn up the volume on the tools all the way. And even that might not make them visible. --Jeff _______________________________________________ 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
