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

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

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.