Boolean formulas for the static identification of injection attacks in Java

Download: PDF, slides (PDF).

“Boolean formulas for the static identification of injection attacks in Java” by Michael D. Ernst, Alberto Lovato, Damiano Macedonio, Ciprian Spiridon, and Fausto Spoto. In LPAR 2015: Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, (Suva, Fiji), Nov. 2015, pp. 130-145.
A previous version appeared as University of Washington Department of Computer Science and Engineering technical report UW-CSE-15-09-03, (Seattle, WA, USA), Sep. 2015.

Abstract

The most dangerous security-related software errors, according to CWE 2011, are those leading to injection attacks — user-provided data that result in undesired database access and updates (SQL-injections), dynamic generation of web pages (cross-site scripting-injections), redirection to user-specified web pages (redirect-injections), execution of OS commands (command-injections), class loading of user-specified classes (reflection-injections), and many others. This paper describes a flow- and context-sensitive static analysis that automatically identifies if and where injections of tainted data can occur in a program. The analysis models explicit flows of tainted data. Its notion of taintedness applies also to reference (non-primitive) types dynamically allocated in the heap, and is object-sensitive and field-sensitive. The analysis works by translating the program into Boolean formulas that model all possible flows. We implemented it within the Julia analyzer for Java and Android. Julia found injection security vulnerabilities in the Internet banking service and in the customer relationship management of a large Italian bank.

Download: PDF, slides (PDF).

BibTeX entry:

@inproceedings{ErnstLMSS2015,
   author = {Michael D. Ernst and Alberto Lovato and Damiano Macedonio and
	Ciprian Spiridon and Fausto Spoto},
   title = {Boolean formulas for the static identification of injection
	attacks in {Java}},
   booktitle = {LPAR 2015: Proceedings of the 20th International
	Conference on Logic for Programming, Artificial Intelligence, and
	Reasoning},
   pages = {130--145},
   address = {Suva, Fiji},
   month = nov,
   year = {2015}
}

(This webpage was created with bibtex2web.)

Back to Michael Ernst's publications.