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