View all Seminars  |  Download ICal for this event

Extending program analysis techniques to web applications and distributed systems

Series: Ph.D. Thesis Defense

Speaker: Ms. Snigdha Athaiya Ph.D student Dept. of CSA

Date/Time: Jan 13 14:30:00

Location: CSA Conference Room, (Room No. 328, Second Floor)

Faculty Advisor: Prof. K V Raghavan

Web-based applications and distributed message-passing systems are two ubiquitous techniques to distribute the execution of an application across multiple machines. Analysis and verification of such programs poses numerous challenges due to the non-linear flow of control and data within the application. In this thesis, we address program analysis problems in the domains of web applications and message-passing systems, and design effective solutions for these problems. Performing end-to-end analysis of web applications using program analysis techniques is a challenge. This is due to multiple reasons, such as client-server interaction, user interaction, and the use of different languages to implement the server-side code and client-side functionality. We propose a technique that translates the entire web application, including server-side and client-side code, into a single-language ``model''. The model is nothing but a standard (i.e., non-web) executable program in the same language as the server-side code. The model is guaranteed to preserve the essential behavioral aspects of the given web application. The upshot is that off-the-shelf tools can be used to analyze the model, without the need to create web-application specific analysis tools. We instantiate our approach in the context of J2EE applications that use JSP to describe pages and Java servlets to implement the server-side code. We have built a tool for the translation of such applications to Java programs. We evaluate our translation tool by converting 5 real world web applications into corresponding Java programs, and, then analyze these programs using three popular third-party program analysis tools - Wala (for static slicing), Java PathFinder (for explicit-state and symbolic model checking), and Zoltar (fault localization by dynamic analysis). With each of these analysis tools we get precise results in most of the cases. Dataflow analysis is a static analysis technique to identify abstract properties of variables at all the points in a program. The second challenge that the thesis addresses is to extend dataflow analysis to distributed asynchronous message-passing systems. Such systems are commonly used to implement distributed mechanisms, protocols, and workflows, in different domains. To obtain good precision, dataflow analysis of message-passing programs needs to somehow skip the traversal of execution paths that read more messages than the number of messages sent so far in the path, as such paths are infeasible at runtime. Current dataflow analysis techniques for message-passing programs either compromise on precision by traversing infeasible paths in addition to feasible paths, or check only simple types of abstract properties (in particular, ones that are representable using finite lattices). This thesis proposes an approach for precise dataflow analysis of message passing asynchronous programs. Our approach traverses only feasible paths, and can check a class of complex abstract properties that need infinite lattice representations. The problem solved by our approach was not known to be decidable so far. Our approach builds on an existing concept in the analysis of parallel systems, namely, coverability, in a novel and involved manner. We have implemented our approach as a tool, and have analyzed its performance on numerous realistic benchmarks. On several of the benchmarks our approach gave more precise results than a baseline analysis that traverses infeasible paths.

Speaker Bio:

Host Faculty: