TitleBoolean formulas for the static identification of injection attacks in Java
Publication TypeConference Paper
Year of Publication2015
AuthorsErnst MD, Lovato A, Macedonio D, Spiridon C, Spoto F
Conference NameLPAR 2015: Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning
Pagination130–145
Date or Month PublishedNovember
Conference LocationSuva, Fiji
AbstractThe 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 (\emphSQL-injec\-tions), dynamic generation of web pages (\emphcross-site scripting-injections), redirection to user-specified web pages (\emphredirect-injections), execution of OS commands (\emphcommand-injections), class loading of user-specified classes (\emphreflection-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.
Downloadshttps://homes.cs.washington.edu/~mernst/pubs/detect-injections-lpar2015.pdf PDF https://homes.cs.washington.edu/~mernst/pubs/detect-injections-lpar2015-... slides (PDF)
Citation KeyErnstLMSS2015