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

PREACH: A Heuristic for Probabilistic Reachability to Identify Hard to Reach Statements

• DOI: 10.1145/3510003.3510227
• 发表时间: 2022-05
• 期刊: 2022 IEEE/ACM 44th International Conference on Software Engineering (ICSE)
• 作者: Seemanta Saha;M. Downing;Tegan Brennan;T. Bultan

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