Authorization Policies in Security-Sensitive Web Services and Applications - Formal Modeling and Analysis

The security of distributed service-oriented applications is crucial in several ap- plications such as e-commerce and e-governance, supporting business and administrative transactions among several parties over the Internet. Their development involves security issues ranging from authentication to the management of the access control on shared resources according to given business and legal models. The specification of security-sensitive applications spans several levels of abstraction, e.g., the protocol for exchanging messages, the set of interface functionalities, the types of the manipulated data, the workflow, the authorization policy, etc. A com- mon design paradigm in distributed applications consists of clearly separating the enforcement of policies at the authorization policy level and of the process work- flow at the workflow level of the applications, so that the interplay between these two levels is abstracted away. While such an approach is attractive because it is quite simple and permits one to reason about crucial properties of the policies un- der consideration, it does not provide the right 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. This thesis focuses on design-time analysis of security-sensitive applications and presents the following main contributions. As the first contribution, I developed a formal framework for the specification and automated analysis of distributed security-sensitive applications organized in two levels: one for the workflow and one for the authorization policies. I formalized the interface functionalities that allow the policy level and the workflow level to interact in a principled way so as to enable the specification of the behavior of distributed systems. As the sec- ond contribution, focusing on the authorization policy level, I proposed a logical framework called DKAL-light, based on the DKAL authorization language, suit- able to specify the dynamic aspects needed to model the communication level and capable to model some forms of human intervention (non-mechanizable activities), e.g. issuing of credentials or certificates, crucial for the correct execution of the system. As the third contribution, I developed “ad-hoc” automated verification techniques for a restricted, but useful in practice, class of secure-sensitive applications in order to solve practical instances of reachability problems I defined. I have also shown how message sequence charts and suitably defined causality graphs can drive and foster the automated verification (by SMT solvers) of security-sensitive applications. Finally, a prototype tool called WSSMT for the mechanization of the two-level framework is presented. As concrete examples, I considered industrial case studies arising in e-business and e-government area in order to show the suitability and flexibility of our approach and our prototype tool.