Verifying the Interplay of Authorization Policies and Workflow in Service-Oriented Architectures

Abstract--A widespread design approach in distributed applications based on the service-oriented paradigm, such as web-services, consists of clearly separating the enforcement of authorization policies and the workflow of the applications, so that the interplay between the policy level and the workflow abstracted away. While such an approach is attractive because it is quite simple and permits one to reason about crucial properties of the policies under consideration, it does not provide t level of abstraction to specify and reason about the way the workflow may interfere with the policies, and vice versa. For example, the creation of a certificate as a side effect of a workflow operation may enable a policy rule to fire and grant access to a certain resource; without executing the operation, the policy rule should remain inactive. Similarly, policy queries may be used as guards for workflow transitions. In this paper, we present a two-level formal verification framework to overcome th...

• Type: Journal
• Year: 2009
• Where: CSE
• Authors: Michele Barletta, Silvio Ranise, Luca Viganò
• Keywords: Authorization Policies, CSE 2009, Policy, Theoretical Computer Science, Workflow