Specification and Verification of Data-driven Web Services

目前，我们正在目睹数据库驱动的Web应用程序的激增，这些应用程序根据相当复杂的工作流程与外部用户或程序进行交互。这种复杂性要求开发能够暴露bug的静态分析技术（例如不符合给定的安全数据访问协议，或不符合预期的业务流程），以增加对安全性的信心，Web应用程序的健壮性和正确性。该项目的总体目标是开发新的工具和技术，用于数据库的高级规范和自动验证，强大的Web应用程序。该项目研究Web服务规范语言的表达能力和验证任务的可行性之间的权衡。它还旨在建立易处理的边界，并开发实用的算法和验证算法。所提出的技术问题将从逻辑、自动机理论、计算复杂性、算法和计算机辅助验证等方面发挥作用。该项目更广泛的影响在于推进开发可信赖的交互式、数据库驱动的Web应用程序所需的技术。这将有利于从数字政府到电子商务到科学应用基础设施的各种应用。这项研究将鼓励数据库和计算机辅助核查界之间更密切的合作。该项目将通过在安全和健全的网络应用程序开发这一关键领域培训博士生和硕士生，促进人力资源开发，并将通过高质量的会议和期刊出版物广泛传播项目成果。开发的工具将通过该项目的网站（http：//www.cs.ucsd.edu/tablsui/project）提供，用于学术、研究和非商业目的。

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 (http://www.cs.ucsd.edu/~lsui/project) for academic, research, and non-commercial purposes.