VAC+: Verifier of Access Control

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

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.