Extending Program Analysis Techniques to Web Applications and Distributed Systems

Abstract

Web-based applications and distributed systems are ubiquitous and indispensable today. These systems use multiple parallel machines for greater functionality, and efficient and reliable computation. At the same time they present innumerable challenges, especially in the field of program analysis. In this thesis, we address two problems in the domain of web based applications and distributed systems relating to program analysis, and design effective solutions for those problems. The first challenge that the thesis addresses is the difficulty of analyzing a web application in an end-to-end manner using a single tool. Such an analysis is hard due to client-server interaction, user interaction, and the use of multiple types of languages, and frameworks in a web application. We propose a semantics preserving modeling technique, that converts a web application into a single-language program. The model of a web application in the thesis is a Java program as we present our modeling technique in the context Java-based web applications. As a result of the translation, off -the-shelf tools available for Java can now be used to analyze the application. We have built a tool for the translation of applications. We evaluate our translation tool by converting 5 real world web applications into corresponding models, and then analyzing the models using 3 popular third-party program analysis tools - Wala (static slicing), Java PathFinder (explicit-state and symbolic model checking), and Zoltar (dynamic fault localization). In all the analysis tools, we get precise results for most cases. The second challenge that the thesis addresses, is the precise data flow analysis of message passing asynchronous systems. Message passing systems are distributed systems, where multiple processes execute concurrently, and communicate with each other by passing messages to the channels associated with each process. These systems encompass majority of the real world distributed systems, e.g., web applications, event-driven programs, reactive systems, etc. Therefore, there is a clear need for robust program analysis techniques for these systems. One such technique is data flow analysis, which statically analyzes a program, and approximates the values of variables in the program due to all runs of the program, using lattices. Any precise data flow analysis needs to account for the blocking of execution in message passing systems, when the required message is not present in the channel. Current data flow analysis techniques for message passing systems either over-approximate the behavior by allowing non-blocking receive operations, or, they are not applicable to general data flow lattices. The thesis proposes algorithms for performing precise data flow analysis of message passing asynchronous programs, using infinite, but finite height lattices. The problem was not known to be decidable before. The algorithm builds on the concepts of parallel systems modeling theory, in a novel and involved manner. We have also made a tool for the algorithm, and have studied its precision and performance by analyzing 10 well-known asynchronous systems and protocols with encouraging results