SHF: Small: Differential Policy Verification and Repair for Access Control in the Cloud

SHF：小型：云中访问控制的差异策略验证和修复

• 批准号: 1817242
• 负责人: Tevfik Bultan
• 金额: $ 50万
• 依托单位: University of California-Santa Barbara
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2018
• 资助国家: 美国
• 起止时间: 2018-07-01 至 2023-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1817242&HistoricalAwards=false
• 关键词: SHF; Small; Differential; Policy; Verification

Due to ubiquitous use of software services, protecting the confidentiality of private information stored in compute clouds is becoming an increasingly critical problem. Users frequently trust sensitive personal information such as financial or medical records to software services. Protection of such private data is of paramount importance for users. In order to prevent disastrous data breaches (which do happen), software developers must accurately specify who can access the data resources and in what ways. Although access control specification languages and libraries provide mechanisms for protecting confidentiality of information in software systems, without automated techniques that can assist developers in writing and checking access control policies, complex policy specifications are likely to have errors that lead to unintended and unauthorized access to data, possibly with disastrous consequences. This project will expose graduate and undergraduate students to security and analysis problems in cloud-based systems through a variety of educational activities including courses, seminars and individual research mentoring.This project develops automated techniques that help software developers in protecting users' data and preventing dangerous exposure ofprivate information. In particular, the investigators develop automated techniques that help software developers in identifying and eliminating errors in access control policies by converting policy specifications to logical constraints and identifying inconsistencies among policies using constraint solving techniques. The project also investigates methods to automatically generating inputs that demonstrate inconsistencies among policies, and automatically generating repairs that remove the inconsistencies among the policies. Within the scope of this project the investigators develop and use novel constraint solving techniques for policy analysis, particularly focusing on analysis of complex numeric and text manipulation operations that are error-prone.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

由于无处不在使用软件服务，保护存储在计算云中的私人信息的机密性正成为越来越关键的问题。 用户经常将敏感的个人信息（例如财务或医疗记录）信任软件服务。 对这种私人数据的保护对于用户来说至关重要。为了防止灾难性的数据泄露（确实发生），软件开发人员必须准确指定谁可以访问数据资源以及以什么方式访问数据资源。尽管访问控制规范语言和库提供了保护软件系统中信息机密性的机制，而没有自动化技术可以帮助开发人员编写和检查访问控制策略，但复杂的策略规格可能会导致意外且未经授权的数据访问数据，可能会带来灾难性的后果。该项目将通过各种教育活动（包括课程，研讨会和个人研究指导）使研究生和本科生在基于云的系统中的安全性和分析问题中，该项目开发自动化技术，以帮助软件开发人员保护用户数据并防止危险的私人信息暴露。 特别是，研究人员开发了自动化技术，可以通过将策略规范转换为逻辑约束并使用约束解决技术之间的策略差异来帮助软件开发人员识别和消除访问控制策略中的错误。该项目还研究了自动生成输入的方法，这些输入证明了策略之间的不一致，并自动生成维修，以消除策略之间的不一致之处。在该项目的范围内，研究人员开发和使用新颖的约束解决技术进行政策分析，尤其是针对容易出错的复杂数字和文本操纵操作的分析。该奖项反映了NSF的法定任务，并被认为是值得通过基金会的知识分子优点和更广泛影响的审查标准来通过评估来获得支持的。

项目成果

Subformula Caching for Model Counting and Quantitative Program Analysis

用于模型计数和定量程序分析的子公式缓存

• DOI: 10.1109/ase.2019.00050
• 发表时间: 2019
• 期刊: 2019 34th IEEE/ACM International Conference on Automated Software Engineering (ASE
• 作者: Eiers, William;Saha, Seemanta;Brennan, Tegan;Bultan, Tevfik
• 通讯作者: Bultan, Tevfik

Quantifying permissiveness of access control policies

量化访问控制策略的允许性

• DOI: 10.1145/3510003.3510233
• 发表时间: 2022
• 期刊: ICSE '22: Proceedings of the 44th International Conference on Software Engineering
• 作者: Eiers, William;Sankaran, Ganesh;Li, Albert;O'Mahony, Emily;Prince, Benjamin;Bultan, Tevfik
• 通讯作者: Bultan, Tevfik

CorbFuzz: Checking Browser Security Policies with Fuzzing

CorbFuzz：通过模糊测试检查浏览器安全策略

• DOI: 10.1109/ase51524.2021.9678636
• 发表时间: 2021
• 期刊: 2021 36th IEEE/ACM International Conference on Automated Software Engineering (ASE
• 作者: Shou, Chaofan;Kadron, Ismet Burak;Su, Qi;Bultan, Tevfik
• 通讯作者: Bultan, Tevfik

Quantitative Policy Repair for Access Control on the Cloud

云上访问控制的定量策略修复

• DOI: 10.1145/3597926.3598078
• 发表时间: 2023
• 期刊: ISSTA 2023
• 作者: Eiers, William;Sankaran, Ganesh;Bultan, Tevfik
• 通讯作者: Bultan, Tevfik

Quacky: Quantitative Access Control Permissiveness Analyzer✱

Quacky：定量访问控制许可分析仪➜±

• DOI: 10.1145/3551349.3559530
• 发表时间: 2022
• 期刊: ASE 2022
• 作者: Eiers, William;Sankaran, Ganesh;Li, Albert;O'Mahony, Emily;Prince, Benjamin;Bultan, Tevfik
• 通讯作者: Bultan, Tevfik