Access Control is concerned with controlling which users of a computer system should have permission to access particular resources such as files. Today, there exists a variety of formal authorization models to meet the wide needs of requirements in specifying access control policies. These include Discretionary Access Control, Mandatory Access Control and Role Based Access Control (RBAC). Recognizing the industry needs, RBAC has been widely deployed in most commercial software including Microsoft Azure, Microsoft Active Directory, and Oracle DBMS. Under RBAC, roles represent organizational agents that perform certain job functions, and permissions to access objects are grouped as roles. Users, in turn, are assigned appropriate roles based on their responsibilities and qualifications. During the past two decades, a number of extensions to the basic RBAC have been made to fit the needs of real-world sectors including mobile, manufacturing, healthcare, and financial services where access permissions need to be granted not only on the basis of roles that individual users possesses but also according to contextual information including the access request time, the user location, sequencing and temporal dependencies between permissions. UK NHS, for instance, implements a variant of RBAC that is able to capture complex policies expressing legitimate relationships and patient consent management.
The need for security analysis: Analysis is essential to understand the implications of access control policies. Although each policy may appear innocent in isolation, their cumulative effect may lead to an undesirable authorization state. A study of the formal behavior of the access control system implemented, helps organizations gain confidence on the level of control they have on the resources they manage. Moreover, security analysis helps designers set policies so that owners do not unknowingly lose control on resources, and make changes to the policies only if the analysis yields no security violations. Policy analysis allows designers to gauge what security breaches could happen if several untrusted users started exploiting the rules to gain unintended permissions in the system. When employees gain more access than necessary, there are several risks: they could abuse that access, or lose information they have access to, or be socially engineered into giving that access to a malfeasant. Unfortunately, security breaches due to unintended access are frequent and can have significant implications including financial and reputation losses. The Vormetric Insider Threat Report (2015) remarks that privilege escalation, where users incrementally gain access rights beyond their requirements, usually as a result of job role changes, is a serious issue for many organizations. The IBM 2016 cyber security report shows that about 60% of recorded attacks have been carried out by insiders. 15% of such attacks involve inadvertent actors, for instance, when users' credentials are lost or stolen. Two recent examples are 1) at Sony when attackers gained unfettered access to the network through a set of stolen credentials, 2) and Home Depot, where a third-party air conditioning supplier with excessive access rights was hacked. Interestingly, the report also shows that the most critical sectors are healthcare, manufacturing and financial services.
Aim of the Project: Several RBAC extensions have been proposed in order to fulfill the requirements of emerging and critical sectors, however, there is a lack of techniques and tools for analysing their security guarantees. The aim of this project is to reduce this key research gap by expanding the real-world scenarios in which security analysis of access control is useful and effective. Specifically, we aim at developing a framework for the security analysis of such policies that features a simple yet expressive for expressing policies as well as scalable solutions for checking their security guarantees.