VAC+: Verifier of Access Control

访问控制涉及控制计算机系统的哪些用户应具有访问特定资源(如文件)的权限。目前，存在各种形式的授权模型来满足指定访问控制策略的广泛需求。其中包括自主访问控制、强制访问控制和基于角色的访问控制(RBAC)。认识到行业需求，RBAC已被广泛部署在大多数商业软件中，包括Microsoft Azure、Microsoft Active Directory和Oracle DBMS。在RBAC中，角色代表执行某些作业功能的组织代理，访问对象的权限被分组为角色。反过来，根据用户的职责和资格，为其分配适当的角色。在过去的二十年中，已经对基本RBAC进行了大量扩展，以适应包括移动、制造、医疗保健和金融服务在内的现实世界部门的需求，其中访问权限不仅需要基于单个用户所拥有的角色，而且需要根据包括访问请求时间、用户位置、顺序和权限之间的时间依赖关系在内的上下文信息来授予。例如，英国NHS实现了RBAC的一个变体，能够捕获表达合法关系和患者同意管理的复杂策略。安全分析的必要性：要了解访问控制策略的含义，分析是必不可少的。尽管每个策略在单独情况下可能看起来是无辜的，但它们的累积效果可能会导致不希望看到的授权状态。对实施的访问控制系统的正式行为的研究有助于组织对其管理的资源的控制级别获得信心。此外，安全分析可帮助设计人员设置策略，使所有者不会在不知情的情况下失去对资源的控制，并且仅在分析未产生安全违规时才对策略进行更改。策略分析使设计人员能够衡量如果几个不受信任的用户开始利用规则获得系统中的意外权限，可能会发生哪些安全漏洞。当员工获得了超过必要的访问权限时，会有几个风险：他们可能会滥用这种访问权限，或者失去他们可以访问的信息，或者被社会工程设计为将这种访问权限授予不法分子。不幸的是，由于意外访问导致的安全漏洞屡见不鲜，可能会产生重大影响，包括财务和声誉损失。Vormetic Insider威胁报告(2015)指出，权限提升对于许多组织来说是一个严重的问题，即用户通常由于工作角色的改变而逐渐获得超出其要求的访问权限。IBM 2016网络安全报告显示，大约60%的有记录的攻击是由内部人士实施的。15%的此类攻击涉及疏忽的行为者，例如，当用户的凭据丢失或被盗时。最近的两个例子是1)在索尼，攻击者通过一套被盗的凭据获得不受限制的网络访问权限；2)家得宝，拥有过多访问权限的第三方空调供应商被黑客攻击。有趣的是，该报告还显示，最关键的行业是医疗保健、制造业和金融服务业。项目目的：为了满足新兴和关键部门的要求，已经提出了几项基于成果的访问控制扩展，但缺乏分析其安全保障的技术和工具。这个项目的目的是通过扩大访问控制安全分析有用和有效的真实世界场景来缩小这一关键研究差距。具体地说，我们的目标是开发一个用于此类策略的安全分析的框架，该框架具有用于表达策略的简单但可表达的特征，以及用于检查其安全保证的可伸缩解决方案。

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.