Seminars

Model Checking Large Complex Web Applications
Masahiro Fujita, University of Tokyo
Sree Rajan, Fujitsu Laboratories of America, Sunnyvale, CA

02/05/2010 – 2pm, GHC 6115

Abstract

Web applications are released to customers in “Beta” mode due to tremendous pressure on “time-to-market”. In order to check end-to-end functional behavior of web applications, conventional testing tools have not matched extremely short release cycles. Formal verification tools such as model checkers and light-weight theorem provers have tried to evolve from small-scale research prototypes to efficient dependable work horses. However, they are still largely perceived as lagging behind conventional testing with respect to usability and scalability, and rightly-so.  In this talk we present the design and architecture of a tool called Web Applications Validation Environment (WEAVE) centered around model checking and symbolic execution for finding bugs in web applications implemented using multiple programming/scripting languages.

In the first part of this talk, we'll discuss the following aspects of WEAVE related to the server-portion of a web application:
(1) An intuitive interface for developers to construct requirements that are compiled into temporal logic to address the issue of usability,
(2) A semi-automatic method for environment generation to constrain the behavior of a (web) client-server application for model checking and
(3) Symbolic execution tailored to finding functional and security bugs. We have successfully applied WEAVE to detect bugs in several large Web applications up to a million lines of code.

In the second part, we'll discuss our approach to the challenges posed by the client portion of a web application such as
(1) JavaScript and flash
(2)Mapping Ajax web page changes to client state changes
(3) Avoiding recrawling the entire web application to regenerate the state model.
In the last part of the talk we'll outline our efforts on deploying verification tools on the cloud, making them available as a service to product groups within Fujitsu.

Biography

Prof. Masahiro Fujita

Masahiro Fujita received his Ph.D. from the University of Tokyo in 1985. He is a professor in VLSI Design and Education Center (VDEC) at the University of Tokyo. Prior to joining the University of Tokyo in 2000, he was director of CAD for VLSI in Fujitsu Laboratories of America for 6 years. He has done innovative works in the areas of digital design verification, synthesis, and testing. He has co-authored 7 books, and has over 100 publications. He has been given several research awards from Japanese scientific societies. His current research interests include synthesis and verification in higher level design stages, hardware/software co-designs and also digital/analog co-designs.

Dr. Sree Rajan

Sree Rajan is a senior researcher at Fujitsu Laboratories of America leading a research program in dependable systems and cloud computing. He joined Fujitsu Laboratories from SRI International Computer Science Laboratory in 1996. His recent research has focused on developing scalable formal techniques to improve trust and security in web applications and cloud computing platforms. Besides his main responsibilities at Fujitsu, he serves as the founding Editor-in-Chief of ACM Transactions on Storage.