Buffer Overrun Detection Using Linear Programming and Static Analysis

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

Proceedings of the 10th ACM Conference on Computer and Communications Security (CCS 2003); pages 345--354; Washington, DC; October 28-30, 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: [ Postscript | PDF | HTML ] (© ACM)
Slides: [ Powerpoint | PDF | HTML ]
DOI: [ 10.1145/948109.948155 ]

Also available as UW-Madison Computer Sciences Department Technical Report 1488, August 2003. This technical report contains a detailed description of some algorithms which are only described in brief in the Proceedings version. Technical Report: [ Postscript | PDF ]

Papers page