Towards practical reactive security audit using extended static checkers

This paper describes our experience of performing it reactive security audit of known security vulnerabilities in core operating system and browser COM components, using an extended static checker HAVOCLITE . We describe the extensions made to the tool to be applicable on such large C++ 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 an effective tool for finding variations of known vulnerabilities. The effort has led to finding and fixing around 70 previously unknown security vulnerabilities in over 10 millions lines operating system and browser code.