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

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

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.