Ambit: Verification of Azure RBAC

In this paper, we present an access control verification approach for Role-Based Access Control (RBAC) mechanisms. Given a specification that models security boundaries (e.g., obtained from a threat model, best practices etc.), we verify that a change to an RBAC state adheres to the specification (i.e., remains within the security boundaries). We demonstrate the practical utility of our approach by instantiating it for Microsoft's Azure AD. We have realized our technique in a tool called Ambit which leverages SMT (Satisfiability Modulo Theory) solvers to efficiently encode and solve the resulting verification problem. We demonstrate the scalability and applicability of our approach with a set of generated benchmarks that attempt to simulate real-world RBAC configurations.