University of California, Santa Barbara

Department of Computer Science

VLab Projects

Current Projects


Project Title: Automata Based String Analysis for Detecting Vulnerabilities in Web Applications

Summary
Web applications contain numerous vulnerabilities that can be exploited by attackers to gain unauthorized access to confidential information and to manipulate sensitive data. Certain input validation vulnerabilities can be automatically identified by means of static code analysis. In particular, data flow analysis can be used to track the flow of potentially malicious data from a source (where user-input is read) to a sink (a sensitive program operation). Traditional data flow analysis considers only binary taint qualifiers, where standard sanitization functions are assumed to convert a tainted (bad) value to an untainted (safe) value. However, such an approach misses certain SQL injection vulnerabilities and cannot identify incorrect sanitization routines. To cover a broader range of security flaws, researchers have proposed to extend data flow analysis with string analysis, a technique that captures the string values that a certain variable might hold at a particular program point. Unfortunately, existing string analysis techniques often make conservative approximations that lead to unnecessarily imprecise results. This makes static vulnerability detection tools report many false positives. In this project, we propose to develop novel techniques for more precise string analysis. To this end, we will use an automata-based approach that represents possible values of a string variable at a program point as a deterministic finite automaton (DFA). Using DFAs, we will develop techniques that support pathsensitivity. To enable precise analysis of loops, we will develop automata-based widening operations. Furthermore, we will extend the basic string analysis techniques to a composite analysis where relationships among string variables and other types of variables can be automatically discovered and analyzed. Using our novel string analysis techniques, false positives due to overly conservative approximations will be significantly reduced. In addition to reducing false positives, we also propose to leverage the results of our precise string analysis to develop novel security solutions and to detect interesting, new classes of vulnerabilities. In particular, we plan to use string analysis to detect malicious file inclusion vulnerabilities. To identify this important type of security problem, it is necessary to possess precise information on the arguments of operations that dynamically load code. Moreover, we propose two novel program capability analyses that use precise string information to gather information about how an application interacts with a back-end database and the file system. This allows us to restrict an application’s database access privileges to a required minimum, and it supports the prevention of directory traversal attacks.

Funding
This project is funded by NSF grant CCF 0916112 (PI: Tevfik Bultan, Co-PI: Chris Kruegel) Period: 2009-2012, Amount: $350,000) provided by Directorate for Computer and Information Science and Engineering (CISE), Division of Computing and Communication Foundations (CCF), Trusted Computing Program.


Project Title: Modeling and Analyzing Trust in Service-Oriented Architectures

Summary
Service-oriented architectures (SOAs) enable the dynamic integration of services implemented on heterogeneous computer systems. An advantage of SOAs is that they provide high-level, semantically-rich services by abstracting the low-level details of their implementation. The availability of useful services such as Google's and Amazon's web service APIs has fostered a number of applications that integrate a number of services to provide novel, more complex functionality. Unfortunately, as is the case with most software, the security of SOAs has been a secondary concern. Most of the security efforts in the SOA community have been focusing on developing web services standards, such as WS-Security, XACML, and SAML. The problem with these standards is that they only specify an acceptable level of practice, not the best practice, and this acceptable level is only achieved if the standard is properly applied. However, experience shows that both web services and service-based applications are often developed under strict time constraints by programmers with little security training. As a result, vulnerable services and service-based applications are deployed and made available to the whole Internet, creating easily-exploitable entry points for the compromise of entire networks. As the service-oriented model is increasingly adopted, there is a need for rigorous approaches to model trust in SOAs and ensure trust in the composition of services, in the form of service-based applications. These approaches should guarantee that by composing services that satisfy certain trust properties one will obtain an application that satisfies the desired trust properties. The goal of this project is to develop novel tools and techniques for the modeling and analysis of trust properties of SOA-based applications. More precisely, the proposed research is to develop a framework that leverages formal models of trust, automated, and interactive verification techniques, and program analysis techniques to address trust properties of single services and of their compositions, at both the interface and implementation levels.

Funding
This project is funded by NSF grant CNS-0716095 (PI: Giovanni Vigna, Co-PIs: Tevfik Bultan, Richard Kemmerer) Period: 2007-2010, Amount: $850,000) provided by Directorate for Computer and Information Science and Engineering (CISE), Division of Compututer and Network Systems (CNS), Cyber Trust Program.


Past Projects


Project Title: Design for Verification

Summary
Developing dependable software is one of the most important challenges in computer science and a scientific approach to design has to address this problem. There has been significant progress in automated verification techniques in recent years, however, scalable software verification remains out of reach. A design for verification approach, which enables software developers to document the design decisions that can be useful during verification, can improve scalability and applicability of automated verification techniques significantly. The approach proposed in this project is to use behavioral interface specifications that support abstraction and modular verification to achieve scalable verification. These specifications will be embedded into the code using design patterns which are geared towards specific classes of verification problems and domain specific verification techniques. Each design pattern will identify the design information necessary to achieve scalable verification in a particular application domain and provide helper classes that will be used to record the required design information in the code. This design information will be used to identify the module boundaries and construct compact models which abstract parts of the code that do not relate to the properties that are being verified. Initial results on application of this approach to verification of synchronization operations in concurrent programs and to verification of interactions among distributed components led to very promising results. These preliminary results suggest that it should be possible to develop a general design for verification framework based on these principles.

Funding
This project is funded by NSF grant CCF-0614002 (PI: Tevfik Bultan, Period: 2006-2008, Amount: $200,000) provided by Directorate for Computer and Information Science and Engineering (CISE), Division of Computing and Communications Foundations (CCF), Science of Design Program.


Project Title: Design for Verification: A New Approach for Developing Highly Dependable Software

Summary
This project will investigate two aspects of design for verification. The first one is enabling software designers to structure the software systems in ways that make them easier to verify. This requires identifying the design principles for developing verifiable systems. The second aspect of design for verification is to elicit extra information from the software designers that would be helpful during automated verification. This requires identifying mechanisms for passing this information obtained during the design phase to the verification phase.

Funding
This project is funded by a grant (PI: Tevfik Bultan, Period: 2006-2007, Amount: $7,000) from Committee on Research, University of California, Santa Barbara.


Project Title: Reliable Concurrent Software Development via Reliable Concurrency Controllers

Summary
Run-time errors in concurrent programs are generally due to wrong usage of synchronization primitives such as monitors. Conventional validation techniques such as testing become ineffective for concurrent programs since the state space increases exponentially with the number of concurrent processes. In recent years there has been considerable progress in automated verification techniques for concurrent systems based on model checking. This project presents a framework for reliable concurrent programming based on interface-based specification and verification of concurrency controllers. Proposed specification and verification techniques for concurrency controllers are modularized by decoupling behavior and interface specifications. The behavior specification is a set of actions (which correspond to methods or procedures) composed of guarded commands. The interface specification is a finite state machine whose transitions represent actions. Concurrency controllers can be designed modularly by composing their interfaces. The proposed approach separates the verification of the concurrency controllers (behavior verification) from the verification of the threads which use them (interface verification). For behavior verification it is possible to use symbolic and infinite-state verification techniques which enables verification of controllers with parameterized constants, unbounded variables and arbitrary number of client threads. For interface verification it is possible to use explicit state program verification techniques which enables verification of arbitrary thread implementations without any restrictions. The correctness of the user threads can be verified using stubs generated from the concurrency controller interfaces which improves the efficiency of the thread verification significantly. It is possible to synthesize efficient Java monitors from the concurrency controller specifications, and the generated implementations preserve the verified properties of the specifications. The proposed framework will be implemented as a set of tools for concurrency controller specification, verification and synthesis.

Selected Publications

Funding
This project is funded by NSF grant CCF-0341365 (PI: Tevfik Bultan, Period: 2003-2007, Amount: $336,000) provided by Directorate for Computer and Information Science and Engineering (CISE), Division of Computing and Communications Foundations (CCF), Trusted Computing Program.


Project Title: Developing Reliable Concurrency-Controllers

Summary
In this project, we use automated verification techniques for developing reliable concurrency-controllers. Concurrency-controllers are software components which are used solely for concurrency control. We propose a modular approach to development of concurrency-controllers which: 1) decouples the behavior and the interface specifications of concurrency-controllers and 2) uses both symbolic and explicit state automated verification techniques by exploiting this separation.

Selected Publications

Funding
This project is funded by a grant (PI: Tevfik Bultan, Period: 2003-2004, Amount: $8,913) from Committee on Research, University of California, Santa Barbara.


Project Title: CAREER: Verifiable Specifications: Tools for Reliable Reactive Software Development

Summary
Developing reliable software for reactive systems is a challenging task. This project focuses on combining and extending the results from two areas which address this problem: 1) specification languages and 2) automated verification methods for reactive systems. Building on the recent results in these areas the goal of this project is to develop verifiable specification languages. This involves research from two directions: 1) From the verification side the goal is to extend the scope of techniques such as model checking to make them applicable to a wider set of systems. 2) From the specification side the goal is to restrict the specification languages as much as possible (without reducing their ability to specify complex systems) in order to make their automated verification feasible. This project addresses both theoretical issues such as complexity and efficiency of model checking techniques, and practical issues such as investigating usability of software specification languages and automated verification techniques in practice.

Selected Publications

Funding
This project is funded by NSF CAREER award CCF-9984822 (PI: Tevfik Bultan, Period: 2000-2004, Amount: $200,000) provided by Directorate for Computer and Information Science and Engineering (CISE), Division of Computing and Communications Foundations (CCF), Software Engineering and Languages Program (SEL).


Project Title: A Composite Model Checking Toolset for Analyzing Software Systems

Summary
The goal of this project is to investigate a new automated verification technique for analyzing software systems called composite model checking. Model checking is a technique for searching the state space of a system to find out if it satisfies a given property. The success of model checking procedures rely on the efficiency of the data structures used to represent the states of the system. In this project a composite model will be developed for combining multiple type-specific representations so that all variable types can be represented efficiently during the state space search. This way, representations such as Binary Decision Diagrams which are efficient for encoding Boolean variables will be combined with representations such as linear arithmetic constraints which can encode unbounded variables. A set of tools will be implemented to support composite model checking. The layered structure of the toolset will allow other researchers to use it at various levels 1) for testing the effectiveness of new representations; 2) for investigating various model checking strategies such as backward and forward search, partitioning and abstraction; or 3) for analyzing complex software specifications.

Selected Publications

Funding
This project is funded by NSF grant CCF-9970976 (PI: Tevfik Bultan, Period: 1999-2003, Amount: $300,000) provided by Directorate for Computer and Information Science and Engineering (CISE), Division of Computing and Communications Foundations (CCF), Software Engineering and Languages Program (SEL).


Project Title: Tools and Techniques for Workflow Specifications

Summary
In this project we investigated the specification and verification techniques for workflow specifications. Workflow systems are used for organizing the execution of multiple tasks, typically in support of a business or scientific process. Since workflow systems involve concurrent execution of multiple tasks, the control logic could easily get complicated. We applied automated verification techniques to workflow systems and developed several heuristics to improve the efficiency of the verification task. In particular, we investigated developing automated verification techniques for a workflow language called Vortex developed at Bell Labs. As a case study, we verified properties of a Vortex specification for an automated help system for customers browsing a web store-front.

Selected Publications

Funding
This project is funded by a grant (PIs: Tevfik Bultan and Jianwen Su, Period: 1999-2000, Amount: $6,000) from Committee on Research, University of California, Santa Barbara.