Team for Research in
Ubiquitous Secure Technology

Citation
Michael Martin. "Automatically Generating Attacks on Webapps with Model Checking". Talk or presentation, 11, October, 2007.

Abstract
Cross-site scripting (XSS) and SQL injection errors are two prominent examples of taint-based vulnerabilities that are responsible for a large number of security breaches in recent years. This paper presents QED, a goal-directed model-checking system for locating software defects including these in large Java web applications.rnrnThe user provides a specification of undesirable behavior and the application to test. Based on the specification and the structure of the web application, QED harnesses the application for model checking and also performs a static analysis to remove unnecessary portions of the search space. The remaining state space can then be systematically checked. This checking is complete enough to also discover defects that only manifest themselves after multiple requests have been made to a web application.rnrnNot only does QED identify these vulnerabilities automatically, it proves the existence of errors by providing an example input of an attack and a program trace showing how the code is compromised. QED does make it easy for the application maintainer to recognize the errors and to make the necessary fix. In other words, unlike many other static analysis tools, QED does not generate any false-positive warnings. For a class of applications, QED can guarantee that it has found all the potential bugs in the program.rnrnQED combines techniques from advanced pointer analysis, dynamic monitoring, and model checking, combining the advantages of all three: QED provides a bound on errors in both directions, and can readily demonstrate how to trigger the bugs it finds.rnrnWe have run QED over a set of 3 Java web applications that use the popular Struts framework. In 130,000 lines of code, we found 10 SQL injections and 13 cross-site scripting errors.

Electronic downloads

• HTML

  Michael Martin. <a
  href="http://www.truststc.org/pubs/302.html"
  ><i>Automatically Generating Attacks on Webapps
  with Model Checking</i></a>, Talk or
  presentation,  11, October, 2007.

• Plain text

  Michael Martin. "Automatically Generating Attacks on
  Webapps with Model Checking". Talk or presentation, 
  11, October, 2007.

• BibTeX

  @presentation{Martin07_AutomaticallyGeneratingAttacksOnWebappsWithModelChecking,
      author = {Michael Martin},
      title = {Automatically Generating Attacks on Webapps with
                Model Checking},
      day = {11},
      month = {October},
      year = {2007},
      abstract = {Cross-site scripting (XSS) and SQL injection
                errors are two prominent examples of taint-based
                vulnerabilities that are responsible for a large
                number of security breaches in recent years. This
                paper presents QED, a goal-directed model-checking
                system for locating software defects including
                these in large Java web applications.rnrnThe user
                provides a specification of undesirable behavior
                and the application to test. Based on the
                specification and the structure of the web
                application, QED harnesses the application for
                model checking and also performs a static analysis
                to remove unnecessary portions of the search
                space. The remaining state space can then be
                systematically checked. This checking is complete
                enough to also discover defects that only manifest
                themselves after multiple requests have been made
                to a web application.rnrnNot only does QED
                identify these vulnerabilities automatically, it
                proves the existence of errors by providing an
                example input of an attack and a program trace
                showing how the code is compromised. QED does make
                it easy for the application maintainer to
                recognize the errors and to make the necessary
                fix. In other words, unlike many other static
                analysis tools, QED does not generate any
                false-positive warnings. For a class of
                applications, QED can guarantee that it has found
                all the potential bugs in the program.rnrnQED
                combines techniques from advanced pointer
                analysis, dynamic monitoring, and model checking,
                combining the advantages of all three: QED
                provides a bound on errors in both directions, and
                can readily demonstrate how to trigger the bugs it
                finds.rnrnWe have run QED over a set of 3 Java web
                applications that use the popular Struts
                framework. In 130,000 lines of code, we found 10
                SQL injections and 13 cross-site scripting errors.},
      URL = {http://www.truststc.org/pubs/302.html}
  }
  

Posted by Larry Rohrbough on 16 Oct 2007.
For additional information, see the Publications FAQ or contact webmaster at www truststc org.