We are currently witnessing a proliferation of database-powered Web applications that interact with external users or programs according to workflows of considerable complexity. This complexity calls for the development of static analysis techniques capable of exposing bugs (such as non-conformance to a given secure data access protocol, or to the intended business process) to increase the confidence in the security, robustness and correctness of Web applications.
The general objective of this project is to develop new tools and techniques for the high-level specification and automatic verification of database-powered Web applications. The project investigates the trade-off between the expressiveness of the Web service specification language and the feasibility of verification tasks. It also aims at establishing tractability boundaries and at developing practical algorithms and heuristics for verification. The technical problems raised bring into play techniques from logic, automata theory, computational complexity, algorithms, and computer-aided verification.
The project's broader impact consists in advancing the technology required by the development of trustworthy interactive, database-powered Web applications. This will benefit a wide variety of applications ranging from digital government to e-commerce to infrastructure for scientific applications. This research will encourage closer collaboration between the database and computer-aided verification communities. The project will contribute to the development of human resources by training doctoral and MS students in the critical area of secure and robust Web application development.
The results of the project will be widely disseminated through high-quality conference and journal publications. The developed tools will be made available via the project's Web site (www.cs.ucsd.edu/~lsui/project) for academic, research, and non-commercial purposes.
