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

La sicurezza di applicazioni distribuite orientate ai servizi è cruciale in diversi ambiti quali l'e-commerce e l'e-governance, capaci di supportare transazioni di carattere finanziario ed amministrativo tra diverse parti in rete. Lo sviluppo di tali applicazioni coinvolge problemi di sicurezza che spaziano dall'autenticazione delle parti coinvolte, alla gestione del controllo degli accessi in accordo con normative finanziarie e legali. La specifica delle applicazioni orientate alla sicurezza si concentra su diversi livelli di astrazione, per esempio, protocolli per lo scambio di messaggi, insiemi di funzionalità di interfaccia, tipi di dati manipolati, flusso di lavoro, policy di autorizzazione, etc. Un comune paradigma di progettazione nelle applicazioni distribuite consiste nel separare in maniera esplicita l'attuazione delle politiche di autorizzazione dal flusso di esecuzione del sistema, non considerando l'interazione tra tali livelli. Nonostante tale approccio sia conveniente in quanto semplice e adatto per ragionare su importanti proprietà delle politiche di autorizzazione, esso non fornisce il giusto livello di astrazione per esaminare l'interazione (a volte subdola) tra i due livelli. Per esempio, la creazione di un certificato come effetto di una istruzione di esecuzione può abilitare una regola di autorizzazione che consenta l'accesso ad una particolare risorsa. Similmente, il risultato di regole di autorizzazione può essere usato come guardia per istruzioni di esecuzione del sistema. La tesi presentata si focalizza sull'analisi a design-time delle applicazioni orientate alla sicurezza, presentando i seguenti contributi. Come primo contributo, ho sviluppato un framework formale per la specifica e la verifica automatica delle applicazioni distribuite orientate alla sicurezza e organizzate in due livelli: un livello di esecuzione (workflow) ed un livello di autorizzazione (authorization policy). Concentrandomi sul livello di autorizzazione, ho progettato un framework chiamato DKAL-Light basato sul linguaggio DKAL, adatto a specificare gli aspetti dinamici della comunicazione e capace di modellare forme di intervento umano durante l'esecuzione automatizzata di tali processi. Ho sviluppato inoltre tecniche "ad hoc" di verifica automatica di proprietà di sicurezza per tali applicazioni. Inoltre, ho proposto l'implementazione di uno strumento (prototipo) chiamato WSSMT per la meccanizzazione del framework a due livelli. Come esempi concreti per mostrare la flessibilità dell'approccio utilizzato, ho considerato casi di studio appartenenti all'e-commerce e all'e-government forniti in ambito industriale.

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.