Verification

The components of a modern web application interact extensively among themselves to generate and customize content for end users. The components perform this interaction by generating invocations using HTML and API based requests. Verifying these invocations is difficult because they are created as a generated object program that is not checked by the web application's compiler. Testing techniques, which are inherently incomplete, typically catch only a subset of these errors. Because of this lack of effective detection techniques, errors in invocation generation have become one of the most common errors made by web application developers.

I developed the waive technique to detect errors related to invocations. waive analyzes a web application to identify the invocations generated at runtime by the application and identifies errors by comparing these against the application's interfaces. The waive technique identifies invocations that are generated directly via API method calls by analyzing the parameters of each call site using string analysis and URL parsing. To identify invocations that are generated via HTML-based requests, waive uses an iterative data-flow analysis that computes a conservative approximation of the HTML pages that could be generated by an application. To make this analysis feasible, waive incorporates several new techniques that I developed, including analysis to reduce the amount of HTML related data propagated by the data-flow functions and a specialized string analysis that allows for context-sensitive evaluation of parametrized HTML fragments. waive also leverages the wam analysis to identify an application's interfaces. To evaluate the usefulness of my technique, I analyzed four subject application with my implementation of waive. I found 133 errors related to invocations in the subject application, while generating only 18 false positives. Many of these invocations represented serious errors that could lead to the generation of incorrect results or crashes in the application.

Papers related to Verification:

Automated Identification of Parameter Mismatches in Web Applications
W. Halfond and A. Orso
Foundations of Software Engineering (FSE 2008).