A comprehensive guide to using Splint. [HTML] [PS] [PDF]

Selected Papers

David Evans and David Larochelle. In IEEE Software, Jan/Feb 2002. (PDF, 12 pages)

Most 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.

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.

Additional Splint Papers

Examples

db: Employee Database Program

Starts with a fully specified, complete implementation. Uses Splint to detect some bugs in the code, detect errors in the specifications, improve the specifications, and adopt and check conformance to a naming convention. (Obsolete, but still mostly relevant.)

Release Notes

Development

SourceForge CVS - latest development version