The reviewed record of science sign in
Pith

arxiv: 2303.16688 · v1 · pith:SPI2OR6G · submitted 2023-03-29 · cs.CR

Model Checking Access Control Policies: A Case Study using Google Cloud IAM

Antonios Gouglidis , Anna Kagia , Vincent C. Hu This is my paper

Reviewed by Pith T0 review T1 audit T2 compute T3 formal T4 kernel pith:SPI2OR6Grecord.jsonopen to challenge →

classification cs.CR
keywords accesscontrolpoliciesmodelcheckingverifygooglesecurity
0
0 comments X
read the original abstract

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.

This paper has not been read by Pith yet.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 4 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. AI Native Asset Intelligence

    cs.CR 2026-05 unverdicted novelty 5.0

    The paper presents a modeling-plus-scoring framework that turns fragmented security signals into stable asset-level importance scores by separating intrinsic exposure from business and data context, evaluated on 131k ...

  2. AI Native Asset Intelligence

    cs.CR 2026-05 unverdicted novelty 5.0

    AI-native asset intelligence framework converts heterogeneous security signals into normalized asset importance scores by separating intrinsic exposure from contextual factors using modeling and deterministic aggregation.

  3. Syntax Is Easy, Semantics Is Hard: Evaluating LLMs for LTL Translation

    cs.LO 2026-04 unverdicted novelty 4.0

    LLMs handle LTL syntax better than semantics, improve with detailed prompts, and perform substantially better when the task is reframed as Python code completion.

  4. Compliance Management for Federated Data Processing

    cs.SE 2026-02 unverdicted novelty 4.0

    A prototype framework collects legal requirements and translates them into machine-actionable policies for federated data processing networks via policy-as-code and LLMs.