VAC+: Verifier of Access Control

VAC：访问控制验证器

• 批准号: EP/P022413/1
• 负责人: Anna Lisa Ferrara
• 金额: $ 12.84万
• 依托单位: University of Southampton
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2017
• 资助国家: 英国
• 起止时间: 2017 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FP022413%2F1
• 关键词: VAC+; Verifier; Access; Control

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.

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

项目成果

Security Analysis of Access Control Policies for Smart Homes

智能家居访问控制策略的安全分析

• DOI: 10.1145/3589608.3593842
• 发表时间: 2023
• 作者: Cimorelli Belfiore R

Data and Applications Security and Privacy XXXI - 31st Annual IFIP WG 11.3 Conference, DBSec 2017, Philadelphia, PA, USA, July 19-21, 2017, Proceedings

数据和应用程序安全与隐私 XXXI - 第 31 届年度 IFIP WG 11.3 会议，DBSec 2017，美国宾夕法尼亚州费城，2017 年 7 月 19-21 日，会议记录

• DOI: 10.1007/978-3-319-61176-1_3
• 发表时间: 2017
• 作者: Uzun E

Bounded Verification of Multi-threaded Programs via Lazy Sequentialization

• DOI: 10.1145/3478536
• 发表时间: 2021-12
• 期刊: ACM Transactions on Programming Languages and Systems (TOPLAS)
• 作者: Omar Inverso;Ermenegildo Tomasco;B. Fischer;Salvatore La Torre;G. Parlato

Parallel bug-finding in concurrent programs via reduced interleaving instances

• DOI: 10.1109/ase.2017.8115686
• 发表时间: 2017-10
• 期刊: 2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE)
• 作者: Truc L. Nguyen;P. Schrammel;B. Fischer;S. L. Torre;G. Parlato