Buffer overrun detection using linear programming and static analysis

Vinod Ganapathy, Somesh Jha, David Chandler, David Melski, and David Vitek.

In 10th ACM Conference on Computer and Communications Security (CCS).

Washington, DC, October 2003.

This paper addresses the issue of identifying buffer overrun vulnerabilities by statically analyzing C source code. We demonstrate a light-weight analysis based on modeling C string manipulations as a linear program. We also present fast, scalable solvers based on linear programming, and demonstrate techniques to make the program analysis context sensitive. Based on these techniques, we built a prototype and used it to identify several vulnerabilities in popular security critical applications.

Paper: [pdf] [ps]
Slides: [ppt] [pdf]

A more detailed version is available as UW-Madison Computer Sciences Technical Report 1488. Refer to this version for the details of some algorithms that were omitted from the conference version of the paper.