A buffer overflow benchmark for software model checkers

Kelvin Ku, Thomas E. Hart, Marsha Chechik, David Lie

Abstract

Software model checking based on abstraction-refinement has recently achieved widespread success in verifying API conformance in device drivers, and we believe this success can be replicated for the problem of buffer overflow detection. This paper presents a publicly-available benchmark suite to help guide and evaluate this research. The benchmark consists of 298 code fragments of varying complexity capturing 22 buffer overflow vulnerabilities in 12 open source applications. We give a preliminary evaluation of the benchmark using the SatAbs model checker

BibTeX

@inproceedings{Ku-al:ASE07,
  author    = {Kelvin Ku and
               Thomas E. Hart and
               Marsha Chechik and
               David Lie},
  title     = {A buffer overflow benchmark for software model checkers},
  booktitle = {ASE},
  pages     = {389--392},
  publisher = {{ACM}},
  year      = {2007},
}

A buffer overflow benchmark for software model checkers

Abstract

Related papers