Authoring access control policies is challenging and prone to misconfigurations. Access control policies must be conflict-free. Hence, administrators should identify discrepancies between policy specifications and their intended function to avoid violating security principles. This paper aims to demonstrate how to formally verify access control policies. Model checking is used to verify access control properties against policies supported by an access control model. The authors consider Google's Cloud Identity and Access Management (IAM) as a case study and follow NIST's guidelines to verify access control policies automatically. Automated verification using model checking can serve as a valuable tool and assist administrators in assessing the correctness of access control policies. This enables checking violations against security principles and performing security assessments of policies for compliance purposes. The authors demonstrate how to define Google's IAM underlying role-based access control (RBAC) model, specify its supported policies, and formally verify a set of properties through three examples.

翻译：编写访问控制策略具有挑战性，且容易产生配置错误。访问控制策略必须无冲突。因此，管理员应识别策略规范与其预期功能之间的差异，以避免违反安全原则。本文旨在展示如何对访问控制策略进行形式化验证。使用模型检测来验证访问控制模型所支持的策略中的访问控制属性。作者以谷歌的云身份与访问管理（IAM）为案例研究，并遵循NIST指南自动验证访问控制策略。使用模型检测进行自动化验证可作为一项有价值的工具，帮助管理员评估访问控制策略的正确性。这使得能够检查违反安全原则的情况，并出于合规目的对策略进行安全评估。作者展示了如何定义谷歌IAM底层基于角色的访问控制（RBAC）模型、指定其支持的策略，并通过三个示例对一组属性进行形式化验证。