Title: Efficient security analysis of Administrative Access Control Policies
Time: 13:00
Location: Meeting room, Building Zeta
Type: Final PhD
Speaker: Enrico Steffinlongo
Abstract: In recent years access control has been a crucial aspect of computer systems, since it is the component responsible for giving users specific permissions enforcing a administrator-defined policy. This lead to the formation of a wide literature proposing and implementing access control models reflecting different system perspectives. Moreover, many analysis techniques have been developed with special attention to scalability, since many security properties have been proved hard to verify. In this setting the presented work provides two main contributions.
In the first, we study the security of workflow systems built on top of a role-based access control in the case of collusion of multiples users. We define a formal model for an ARBAC based workflow system and we state
a notion of security against collusion. Furthermore we propose a scalable static analysis technique for proving the security of a workflow. Finally we implement it in a prototype tool showing its effectiveness.
In the second contribution, we propose a new model of administrative attribute-based access control (AABAC) where administrative actions are enabled by boolean expressions predicating on user attributes values. Subsequently we introduce two static analysis techniques for the verification of reachability problem: one precise, but bounded, and one over-approximated. We also give a set of pruning rules in order to reduce the size of the problem increasing scalability of the analysis. Finally, we implement the analysis in a tool and we show its effectiveness on several realistic case studies.
Tag Archives: Access Control
25/02/2015 Talk by Stefano Calzavara
Title: Compositional Typed Analysis of ARBAC Policies
Time: 14:00
Location: Meeting room
Type: Research Result
Speaker: Stefano Calzavara
Abstract:
Model-checking is a popular approach to the security analysis of ARBAC policies, but its effectiveness is hindered by the exponential explosion of the ways in which different users can be assigned to different role combinations. In this talk we propose a paradigm shift, based on the observation that, while verifying ARBAC by exhaustive state search is complex, realistic policies often have rather simple security proofs, and we propose to use types as an effective tool to leverage this simplicity. Concretely, we present a static type system to verify the security of ARBAC policies, along with a sound and complete type inference algorithm used to automate the verification process. We then introduce compositionality results, which identify sufficient conditions to preserve the security guarantees obtained by the verification of different sub-policies when these sub-policies are combined together: this compositional reasoning is crucial when policy administration is highly distributed and naturally supports the security analysis of evolving ARBAC policies. We evaluate our approach by implementing TAPA, a static analyser for ARBAC policies based on our theory, which we test on a number of relatively large, publicly available policies from the literature.
