Buffer Overrun Detection Using Linear Programming and Static Analysis

Abstract

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.