Seminars
View all Seminars | Download ICal for this eventExtending 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
Abstract:
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: