University of California, Santa Barbara

Department of Computer Science

Research at VLab

New NSF grant to VLab is in the news: See here and here

Our research focuses on automated verification techniques and their application to software. As computer systems become more pervasive, their dependability becomes increasingly important. As a result, there is an ongoing shift in focus, both in academia and industry, from performance to dependability. The size and complexity of the software systems nowadays inevitably lead to errors during both design and implementation phases. The goal of our research at VLab is to develop verification techniques that will help developers in identifying errors in software. Our recent focus has been on software applications that use the three-tier architecture and software-as-service paradigm. Here are some of the research topics we work on: string analysis, data model verification, analyzing service oriented and distributed systems, design for verification, and infinite state verification.

String Analysis: Web applications provide critical services over the Internet and frequently handle sensitive data. Unfortunately, web application development is error prone and results in applications that are vulnerable to attacks by malicious users. The global accessibility of critical web applications make this an extremely serious problem. Most critical web application vulnerabilities such as Cross Site Scripting (XSS), SQL command injection (SQLCI) and Malicious File Execution (MFE) are due to improper use and sanitization of strings. We have developed string analysis techniques that automatically 1) identify if a web application is vulnerable to attacks due to string manipulation errors, 2) if a web application is vulnerable, generate characterization of user inputs that might exploit that vulnerability (vulnerability signatures), and 3) generate patches that repair the vulnerability. Our string analysis approach is based on automata, where values that string expressions can take at each program point are characterized as deterministic finite automata (DFA). We developed symbolic forward and backward reachability analyses using DFA as a symbolic representation. We implemented our analysis approach in a tool called Stranger that analyzes PHP programs. More recently we extended our results on string analysis to relational string analysis, automated string abstractions, client-side string analysis (for JavaScript) and differential string analysis.

Data Model Verification: The growing influence of web applications in every aspect of society makes their dependability an immense concern. One positive advancement in web application development has been the adoption of the Model-View-Controller (MVC) pattern. Many popular web application development frameworks such as Ruby on Rails, Zend for PHP, CakePHP, Django for Python, and Spring for J2EE are based on the MVC pattern. A fundamental building block of web the MVC pattern is the data model, which specifies the object classes and the relations among them. The MVC pattern facilitates the separation of the data model (Model) from the user interface logic (View) and the control flow logic (Controller). The modularity and separation of concerns principles imposed by the MVC pattern provide opportunities for developing customized verification and analysis techniques. MVC-based frameworks use an object-relational mapping (ORM) to map the data representation of the web application to the back-end database. We developed an approach for automated verification of data models that 1) extracts a formal data model from the given ORM specification, 2) converts verification queries about the data model to queries about the satisfiability of formulas in a decidable theory, and 3) uses a decision procedure to check the satisfiability of the resulting formulas. We implemented this approach and applied it to open-source Rails applications, discovering data model errors in existing applications and demonstrating the feasibility of our approach.

Analyzing Service-Oriented and Distributed Systems: Service-oriented systems are distributed software systems that consist of web accessible software components (services) that interact with each other via messages sent over the Internet. A fundamental problem in developing reliable web services is analyzing their interactions. This a challenging problem due to the distributed nature of web services. We developed a framework for modeling, specifying and analyzing interactions of web services. We addressed some fundamental problems in this area such as realizability of top-down specifications and synchronizability of asynchronously communicating web services. We developed a tool called Web Service Analysis Tool (WSAT) which verifies properties about interactions of web services and checks sufficient conditions for realizability and synchronizability. Decidability of the realizability and synchronizability problems remained open for several years and recently we were able to give algorithms for solving these problems, proving their decidability. Our results in this domain turned out to be influential in other domains (for example for analyzing channel contracts in Singularity operating system.)

Design for Verification: A promising approach in attacking the dependability problem is to find ways of constructing software that facilitate automated verification. We developed a design for verification approach by introducing a set of design patterns which support a modular verification strategy. Our approach builds on the following principles: 1) use of stateful, behavioral interfaces which isolate the behavior and enable modular verification, 2) an assume-guarantee style verification strategy which separates verification of the behavior from the verification of the conformance to the interface specifications, 3) a general model checking technique for interface verification, and 4) domain specific and specialized verification techniques for behavior verification. So far, we applied this approach to verification of concurrent and distributed systems which are especially challenging to get right. The case studies we conducted show that, using our design for verification approach, it is possible to achieve scalable software verification in these application domains.

Infinite State Verification: One direction of research at VLab addresses fundamental limitations of automated verification which hinder its applicability to software. One such limitation is the fact that software systems have data-types which have arbitrarily large domains and well known theoretical results show that automated verification of such systems is impossible. Our research on verification techniques for infinite state systems lead to heuristic solutions to this problem which identify the errors that are encountered in practice. The main idea is to search an infinite state space using conservative approximations which over or under-approximate the behaviors of a system and can be used both to guarantee the absence of bugs (via over-approximation) and to identify the existing bugs (via under-approximation). We developed a tool called Action Language Verifier (ALV) which implements these heuristics and we applied ALV to verification of various software systems.