FMitF: Track II: SMT-Based Reachability Analyzer of NGAC Policies

FMitF：轨道 II：NGAC 策略的基于 SMT 的可达性分析器

• 批准号: 2318891
• 负责人: Dianxiang Xu
• 金额: $ 10万
• 依托单位: University of Missouri-Kansas City
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-07-01 至 2024-12-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2318891&HistoricalAwards=false
• 关键词: FMitF; Track; II; SMT; Based

Access control is a crucial security mechanism that ensures appropriate user authorization within computer systems. To achieve accountability and privacy, access control methods must associate obligations with privileges. The Next Generation Access Control (NGAC) standard, developed by the American National Standards Institute, introduces an innovative approach by extending obligations as a programming mechanism. This allows for real-time adjustment of privileges to accommodate evolving operational requirements. However, designing and implementing an NGAC policy manually can be error prone. Identifying privilege changes associated with access events, specifying them with obligations, and verifying the resulting policy for correctness present significant challenges. Errors in the policy can have severe consequences for the authorization state. Therefore, it is crucial to explore efficient methodologies for developing error-free NGAC policies. This project aims to address this gap by leveraging SMT (Satisfiability Modulo Theories), a mathematically based method, to verify operational NGAC systems and uncover potential errors.The project's main objective is to develop an open-source reachability analyzer that allows users to interact with, analyze, and understand the behavior of complex NGAC policies. This analyzer will facilitate correct policy implementation by utilizing an SMT solver to examine the sequences of configuration changes triggered by access events that activate obligations. A significant innovation lies in formalizing the procedural actions of administrative obligations using the declarative SMT language, which alters the SMT formulas representing the authorization configurations. To ensure usability and accessibility within the NGAC community, the tool will provide a user-friendly interface for end-users and an application programming interface (API) for developers. By integrating the results with education, the project aims to utilize the tool and case studies in software security courses. Additionally, the formal verification of NGAC policies will be introduced in the next edition of the software engineering textbook authored by one of the investigators, further promoting knowledge dissemination and adoption of best practices.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.

访问控制是一种至关重要的安全机制，可确保计算机系统中的用户授权适当。为了实现问责制和隐私，访问控制方法必须将义务与特权联系起来。由美国国家标准研究所（American National Standards Institute）开发的下一代访问控制（NGAC）标准，通过扩展义务作为编程机制，引入了一种创新的方法。这允许对特权进行实时调整以适应不断发展的操作要求。但是，手动设计和实施NGAC策略可能是错误的。确定与访问事件相关的特权更改，用义务指定它们，并验证由此产生的策略提出重大挑战。政策中的错误可能会对授权州造成严重后果。因此，探索有效的方法学对于制定无错误的NGAC策略至关重要。该项目旨在通过利用基于数学的方法（一种基于数学的方法）来验证操作NGAC系统并发现潜在错误的方法来解决这一差距。该项目的主要目标是开发开源的无覆盖范围分析仪，使用户可以与用户进行互动，分析并了解复杂的NGAC策略的行为。该分析仪将通过利用SMT求解器来检查配置序列的序列变化，该序列由激活义务的访问事件触发。一项重大创新在于使用声明性SMT语言正式化行政义务的程序行动，该语言的语言改变了代表授权配置的SMT公式。为了确保NGAC社区内的可用性和可访问性，该工具将为最终用户提供用户友好的接口，并为开发人员提供应用程序编程界面（API）。通过将结果与教育相结合，该项目旨在利用软件安全课程中的工具和案例研究。此外，NGAC政策的正式验证将在下一版的软件工程教科书中介绍，其中一位调查人员撰写，进一步促进知识传播和最佳实践的采用。该奖项反映了NSF的法定任务，并被认为是通过该基金会的知识分子功能和广泛的影响来评估CRITERIA的评估。