A type system for format strings

Download: PDF, slides (PDF), slides (ODP), demo paper (PDF), Format String Checker implementation.

“A type system for format strings” by Konstantin Weitz, Gene Kim, Siwakorn Srisakaokul, and Michael D. Ernst. In ISSTA 2014, Proceedings of the 2014 International Symposium on Software Testing and Analysis, (San Jose, CA, USA), July 2014, pp. 127-137.
A tool demonstration appeared as “A format string checker for Java” by Konstantin Weitz, Gene Kim, Siwakorn Srisakaokul, and Michael D. Ernst. In ISSTA 2014, Proceedings of the 2014 International Symposium on Software Testing and Analysis, (San Jose, CA, USA), July 2014, pp. 441-444.

Abstract

Most programming languages support format strings, but their use is error-prone. Using the wrong format string syntax, or passing the wrong number or type of arguments, leads to unintelligible text output, program crashes, or security vulnerabilities.

This paper presents a type system that guarantees that calls to format string APIs will never fail. In Java, this means that the API will not throw exceptions. In C, this means that the API will not return negative values, corrupt memory, etc.

We instantiated this type system for Java's Formatter API, and evaluated it on 6 large and well-maintained open-source projects. Format string bugs are common in practice (our type system found 104 bugs), and the annotation burden on the user of our type system is low (on average, for every bug found, only 1.0 annotations need to be written).

Download: PDF, slides (PDF), slides (ODP), demo paper (PDF), Format String Checker implementation.

BibTeX entry:

@inproceedings{WeitzKSE2014,
   author = {Konstantin Weitz and Gene Kim and Siwakorn Srisakaokul and
	Michael D. Ernst},
   title = {A type system for format strings},
   booktitle = {ISSTA 2014, Proceedings of the 2014 International
	Symposium on Software Testing and Analysis},
   pages = {127--137},
   address = {San Jose, CA, USA},
   month = jul,
   year = {2014}
}

(This webpage was created with bibtex2web.)

Back to Michael Ernst's publications.