Improving computer security using extended static checking

I describe a method for finding security flaws in source code by way of static analysis. The method is notable because it allows a user to specify a wide range of security properties while also leveraging a set of predefined common flaws. It works by using an automated theorem prover to analyze verification conditions generated from C source code and a set of specifications that define security properties. In order to help lower the cost of using the checker, I present a method for automatically generating application-specific specifications based on a generic specification library. I demonstrate that the method can be used to identify real vulnerabilities in real programs.