WSSMT: Towards the Automated Analysis of Security-Sensitive Services and Applications

The security of service-oriented applications is crucial in several contexts such as e-commerce or e-governance. The design, implementation, and deployment of this kind of services are often so complex that serious vulnerabilities remain even after extensive application of traditional validation techniques, such as testing. Given the importance of security-sensitive service applications, the development of techniques for their automated validation is growing. In this paper, we illustrate our formal framework to the specification and validation of security-sensitive applications structured in two levels: the workflow level (dealing with the control of flow and the manipulation of data) and the policy level (describing trust relationships and access control). In our framework, verification problems are reduced to logical problems whose decidability can be shown under suitable assumptions, which permit the validation of practically relevant classes of services. As a by-product, it is possible to re-use state-of-the-art theorem-proving technology to mechanize the verification process. This is the idea underlying our prototype validation tool WSSMT, "Web-Service (validation by) Satisfiability Modulo Theories\´\´, which has been successfully used on two industrial case studies taken from the FP7 European project AVANTSSAR.