Automata-based verification of security requirements of composite web services

With the increasing reliance of complex real-world applications on composite web services assembled from independently developed component services, there is a growing need for effective approaches to verifying that a composite service not only offers the required functionality but also satisfies the desired non-functional requirements (NFRs). In high-assurance applications such as traffic control, medical decision support, and coordinated response to civil emergencies, of special concern are NFRs having to do with security, safety and reliability of composite services. Current approaches to verifying NFRs of composite services (as opposed to individual services) remain largely ad-hoc and informal in nature. In this paper we develop techniques for ensuring that a composite service meets the user-specified NFRs expressible in the form of hard constraints e.g., "response time has to be less than 5 minutes." We introduce an automata-based framework for verifying that a composite service satisfies the desired NFRs based on the known guarantees regarding the non-functional properties of the component services. We further show how to improve the efficiency of verifying that a composite service indeed satisfies a desired set of NFRs by: (i) Exploiting information about the applicability of specific NFRs (e.g., security) only to certain subsets of the component services that make up a composite service to minimize the verification effort and (ii) Identifying inconsistencies between NFRs with overlapping scopes. We illustrate how our approach can be used to verify the security requirements for an Emergency Management System. We also show how the approach can be used to verify whether a composite service satisfies any desired set of NFRs that can be expressed in the form of hard constraints of a quantitative nature.