Security audit using extended static checking: Is it cost-effective yet?

This paper describes our experience of doing variation analysis of known security vulnerabilities in C++ projects including core OS and browser COM components, using an extended static checker HAVOC-LITE. We describe the extensions made to the tool to be applicable on such large components, along with our experience of using an extended static checker in the large. We argue that the use of such checkers as a configurable static analysis in the hands of security auditors can be quite cost-effective tool for finding variations of known vulnerabilities.