Buffer overrun detection using linear programming and static analysis

Vinod Ganapathy; Somesh Jha; David Chandler; David Melski; David Vitek

doi:10.1145/948152.948155

Buffer overrun detection using linear programming and static analysis

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

Research output: Contribution to journal › Conference article › peer-review

67 Scopus citations

Abstract

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.

Original language	English (US)
Pages (from-to)	345-354
Number of pages	10
Journal	Proceedings of the ACM Conference on Computer and Communications Security
DOIs	https://doi.org/10.1145/948152.948155
State	Published - 2003
Externally published	Yes
Event	Proceedings of the 10th ACM Conference on Computer and Communications Security, CCS 2003 - Washington, DC, United States Duration: Oct 27 2003 → Oct 31 2003

All Science Journal Classification (ASJC) codes

Software
Computer Networks and Communications

Keywords

Buffer overruns
Linear programming
Static analysis

Access to Document

10.1145/948152.948155

Cite this

@article{71997420aa274eafbd497d72ebd4729e,

title = "Buffer overrun detection using linear programming and static analysis",

abstract = "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.",

keywords = "Buffer overruns, Linear programming, Static analysis",

author = "Vinod Ganapathy and Somesh Jha and David Chandler and David Melski and David Vitek",

year = "2003",

doi = "10.1145/948152.948155",

language = "English (US)",

pages = "345--354",

journal = "Proceedings of the ACM Conference on Computer and Communications Security",

issn = "1543-7221",

publisher = "Association for Computing Machinery (ACM)",

note = "Proceedings of the 10th ACM Conference on Computer and Communications Security, CCS 2003 ; Conference date: 27-10-2003 Through 31-10-2003",

}

TY - JOUR

T1 - Buffer overrun detection using linear programming and static analysis

AU - Ganapathy, Vinod

AU - Jha, Somesh

AU - Chandler, David

AU - Melski, David

AU - Vitek, David

PY - 2003

Y1 - 2003

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

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

KW - Buffer overruns

KW - Linear programming

KW - Static analysis

UR - http://www.scopus.com/inward/record.url?scp=3142582577&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=3142582577&partnerID=8YFLogxK

U2 - 10.1145/948152.948155

DO - 10.1145/948152.948155

M3 - Conference article

AN - SCOPUS:3142582577

SN - 1543-7221

SP - 345

EP - 354

JO - Proceedings of the ACM Conference on Computer and Communications Security

JF - Proceedings of the ACM Conference on Computer and Communications Security

T2 - Proceedings of the 10th ACM Conference on Computer and Communications Security, CCS 2003

Y2 - 27 October 2003 through 31 October 2003

ER -

Buffer overrun detection using linear programming and static analysis

Abstract

All Science Journal Classification (ASJC) codes

Keywords

Access to Document

Other files and links

Fingerprint

Cite this