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.

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