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

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.