Buffer Overrun Detection Using Linear Programming and Static Analysis
Vinod Ganapathy, Somesh Jha, David Chandler, David Melski, David Vitek
This paper addresses the issue of identifiing buffer overrun vulnerabilities by statically analyzing C source code. We demonstrate a scalable analysis based on modeling C string manipulations as a linear program. We also present fast, scalable solvers based on linear programming, and demonstrate how to make the analysis context sensitive. Based on these techniques, we built a prototype and used it to identify several vulnerabilities in popular security critical applications.
Download this report (PDF)
Return to tech report index