Formal Verification of Cloud RBAC Policies for Secure Google IAM Configurations

• Jitendra Gupta

  Compunnel Inc.

  Author

Misconfigured access control policies remain a leading cause of security breaches in cloud environments, yet administrators lack systematic tools for rigorous validation of complex policy sets. This paper introduces a formal verification framework for Google Cloud Identity and Access Management (IAM) that precisely models its role-based access control (RBAC) semantics, including hierarchical resource structures (organization, folders, projects, resources), policy inheritance rules, and conditional bindings. The proposed RBAC\textsubscript{GCP} model is operationalized as a transition system, enabling automated model checking against security properties expressed in Computation Tree Logic (CTL). We implement the framework using the NuSMV symbolic model checker and evaluate it on three realistic Google Cloud scenarios: Cloud Pub/Sub messaging, Cloud Storage, and Compute Engine virtual machines. The case studies demonstrate the framework's ability to detect unintended permission inheritance, cross-branch privilege leaks, violations of least privilege, and separation-of-duty constraints. When a property fails, the model checker generates a concrete counterexample that pinpoints the exact member, resource, permission, and inheritance path responsible, transforming verification into an actionable remediation tool. The results show that formal verification can serve as an effective cybersecurity tool for proactive assessment of cloud access configurations, supporting compliance audits and preventing data breaches before policy deployment.

• PDF

Copyright (c) 2026 International Journal of Intelligent Systems and Data Science

This work is licensed under a Creative Commons Attribution 4.0 International License.