Specification and Verification of Data-driven Web Services

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