Loop-extended symbolic execution on binary programs

Prateek Saxena, Pongsin Poosankam, Stephen McCamant, Dawn Song

Research output: Chapter in Book/Report/Conference proceedingConference contribution

107 Scopus citations

Abstract

Mixed concrete and symbolic execution is an important technique for finding and understanding software bugs, including securityrelevant ones. However, existing symbolic execution techniques are limited to examining one execution path at a time, in which symbolic variables reflect only direct data dependencies. We introduce loop-extended symbolic execution, a generalization that broadens the coverage of symbolic results in programs with loops. It introduces symbolic variables for the number of times each loop executes, and links these with features of a known input grammar such as variable-length or repeating fields. This allows the symbolic constraints to cover a class of paths that includes different numbers of loop iterations, expressing loop-dependent program values in terms of properties of the input. By performing more reasoning symbolically, instead of by undirected exploration, applications of loop-extended symbolic execution can achieve better results and/or require fewer program executions. To demonstrate our technique, we apply it to the problem of discovering and diagnosing buffer-overflow vulnerabilities in software given only in binary form. Our tool finds vulnerabilities in both a standard benchmark suite and 3 real-world applications, after generating only a handful of candidate inputs, and also diagnoses general vulnerability conditions.

Original languageEnglish (US)
Title of host publicationProceedings of the 18th International Symposium on Software Testing and Analysis, ISSTA 2009
PublisherAssociation for Computing Machinery, Inc
Pages225-235
Number of pages11
ISBN (Electronic)9781605583389
DOIs
StatePublished - Jul 19 2009
Event18th International Symposium on Software Testing and Analysis, ISSTA 2009 - Chicago, United States
Duration: Jul 19 2009Jul 23 2009

Publication series

NameProceedings of the 18th International Symposium on Software Testing and Analysis, ISSTA 2009

Other

Other18th International Symposium on Software Testing and Analysis, ISSTA 2009
CountryUnited States
CityChicago
Period7/19/097/23/09

Fingerprint Dive into the research topics of 'Loop-extended symbolic execution on binary programs'. Together they form a unique fingerprint.

  • Cite this

    Saxena, P., Poosankam, P., McCamant, S., & Song, D. (2009). Loop-extended symbolic execution on binary programs. In Proceedings of the 18th International Symposium on Software Testing and Analysis, ISSTA 2009 (pp. 225-235). (Proceedings of the 18th International Symposium on Software Testing and Analysis, ISSTA 2009). Association for Computing Machinery, Inc. https://doi.org/10.1145/1572272.1572299