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.

• Type: Journal
• Year: 2002
• Where: SP
• Authors: Brian Chess
• Keywords: Automated Theorem Prover, Security Privacy, Security Properties, Source Code, SP 2002