Title :
Improving computer security using extended static checking
Author_Institution :
Dept. of Comput. Eng., California Univ., Santa Cruz, CA, USA
fDate :
6/24/1905 12:00:00 AM
Abstract :
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.
Keywords :
formal specification; formal verification; program diagnostics; security of data; theorem proving; C source code; automated theorem prover; computer security; extended static checking; security flaws; source code; specifications; static analysis; verification conditions; Computer errors; Computer security; Error correction; Information security; Inspection; Java; Programming profession; Prototypes; Software libraries; Writing;
Conference_Titel :
Security and Privacy, 2002. Proceedings. 2002 IEEE Symposium on
Print_ISBN :
0-7695-1543-6
DOI :
10.1109/SECPRI.2002.1004369
