Improving computer security using extended static checking

We 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. We demonstrate that the method can be used to identify real vulnerabilities in real programs.