Pith. sign in

REVIEW 4 cited by

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

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

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
classification cs.CR
keywords accesscontrolpoliciesmodelcheckingverifygooglesecurity
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved
0 comments
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.

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.