Automatic Generation of XSS and SQL Injection Attacks with Goal-Directed Model Checking

Cross-site scripting (XSS) and SQL injection errors are two prominent examples of taint-based vulnerabilities that have been responsible for a large number of security breaches in recent years. This paper presents QED, a goal-directed model-checking system that automatically generates attacks exploiting taint-based vulnerabilities in large Java web applications. This is the first time where model checking has been used successfully on real-life Java programs to create attack sequences that consist of multiple HTTP requests. QED accepts any Java web application that is written to the standard servlet specification. The analyst specifies the vulnerability of interest in a specification that looks like a Java code fragment, along with a range of values for form parameters. QED then generates a goal-directed analysis from the specification to perform session-aware tests, optimizes to eliminate inputs that are not of interest, and feeds the remainder to a model checker. The checker will sy...

• Type: Conference
• Year: 2008
• Where: USS
• Authors: Michael C. Martin, Monica S. Lam
• Keywords: Cross-site Scripting, Java Web Applications, Operating System, Taint-based Vulnerabilities, USS 2008