David Evans and David Larochelle. In IEEE Software, Jan/Feb 2002. (PDF, 12 pages)Statically Detecting Likely Buffer Overflow VulnerabilitiesMost security attacks exploit instances of well-known classes of implementations flaws. This article describes how Splint can be used to detect common security vulnerabilities (including buffer overflows and format string vulnerabilities).
David Larochelle and David Evans. In 2001 USENIX Security Symposium, Washington, D. C., August 13-17, 2001. (PDF, HTML, 13 pages) ( Talk slides [PPT] [PDF])Buffer overflow attacks may be today's single most important security threat. This paper presents a new approach to mitigating buffer overflow vulnerabilities by detecting likely vulnerabilities through an analysis of the program source code. Our approach exploits information provided in semantic comments and uses lightweight and efficient static analyses. This paper describes an implementation of our approach that extends the LCLint annotation-assisted static checking tool. Our tool is as fast as a compiler and nearly as easy to use. We present experience using our approach to detect buffer overflow vulnerabilities in two security-sensitive programs.
Annotation-Assisted Lightweight Static Checking
David Evans. The First International Workshop on Automated Program Analysis, Testing and Verification (ICSE 2000). Feb 25, 2000.A short position paper describing the research agenda behind LCLint.
Static Detection of Dynamic Memory Errors
David Evans. In SIGPLAN Conference on Programming Language Design and Implementation (PLDI '96), Philadelphia, PA, May 1996. (PDF, gzipped postscript; 10 pages)Describes approach for exploiting annotations added to code to detect a wide class of errors, focusing on memory management concerns.
LCLint: A Tool for Using Specifications to Check Code
David Evans, John Guttag, Jim Horning and Yang Meng Tan, SIGSOFT Symposium on the Foundations of Software Engineering, December 1994. (PDF, gzipped postscript; 10 pages)An introduction to LCLint from a software engineering perspective. Shows how LCLint can be used to improve a small sample program.
Static Error Checking of C Applications Ported from UNIX to WIN32 Systems Using LCLint, March 2001. [PDF, Word]
Christopher Barker, UVA Bachelor of Science in Computer Engineering, March 2001.Using Specifications to Check Source CodeDescribes process and experience using LCLint meta-annotations to define and use annotations designed to assist the process of porting applications. (Some of the LCLint features described in this report are not yet available in the public release. Contact [email protected] if you are interested in using a pre-release version.)
David Evans, MIT/LCS/TR-628, June 1994, SM Thesis.MIT Master's Thesis on LCLint. Detailed description of the motivation and use of LCLint (but somewhat out of date).
Undergratuate Theses in Progress:
Secure Programming Group, 2002. (HTML, PDF, postscript)LCLint User's GuideA comprehensive guide to using Splint.
David Evans, 1996-2000. (HTML, PDF, postscript)A comprehensive guide to using LCLint (superceded by Splint Manual).