Splint Publications

Refereed Papers

Improving Security Using Extensible Lightweight Static Analysis

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

Statically Detecting Likely Buffer Overflow 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.

Theses

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.

Describes 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 lclint@cs.virginia.edu if you are interested in using a pre-release version.)

Using Specifications to Check Source Code

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:

• David Friedman - investigating effectiveness of static analysis in security
• Michael Lanouette - Static Checking of Coding Standards
• Hien Phan - Developing a Web Interface for the LCLint Static Checker

Manual

Splint Manual

Secure Programming Group, 2002. (HTML, PDF, postscript)

A comprehensive guide to using Splint.

LCLint User's Guide

David Evans, 1996-2000. (HTML, PDF, postscript)

A comprehensive guide to using LCLint (superceded by Splint Manual).

	Splint - Secure Programming Lint evans@virginia.edu Download - Documentation - Manual - Links Source - Linux - Publications - Talks Reporting Bugs    Sponsors - Credits