Home > Research > Publications & Outputs > Model Checking Access Control Policies

Research

Electronic data

Text available via DOI:

Keywords

View graph of relations

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

Research output: Working paper › Preprint

Published

Standard

Model Checking Access Control Policies: A Case Study using Google Cloud IAM. / Gouglidis, Antonios; Kagia, Anna; Hu, Vincent C.
Arxiv, 2023.

Research output: Working paper › Preprint

Harvard

Gouglidis, A, Kagia, A & Hu, VC 2023 'Model Checking Access Control Policies: A Case Study using Google Cloud IAM' Arxiv. https://doi.org/10.48550/arXiv.2303.16688

APA

Gouglidis, A., Kagia, A., & Hu, V. C. (2023). Model Checking Access Control Policies: A Case Study using Google Cloud IAM. Arxiv. https://doi.org/10.48550/arXiv.2303.16688

Vancouver

Gouglidis A, Kagia A, Hu VC. Model Checking Access Control Policies: A Case Study using Google Cloud IAM. Arxiv. 2023 Mar 29. doi: https://doi.org/10.48550/arXiv.2303.16688

Author

Gouglidis, Antonios ; Kagia, Anna ; Hu, Vincent C. / Model Checking Access Control Policies : A Case Study using Google Cloud IAM. Arxiv, 2023.

Bibtex

@techreport{afc7cda3b8184cbeb9ce0e10da8ca77e,
title = "Model Checking Access Control Policies: A Case Study using Google Cloud IAM",
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.",
keywords = "cs.CR",
author = "Antonios Gouglidis and Anna Kagia and Hu, {Vincent C.}",
year = "2023",
month = mar,
day = "29",
doi = "https://doi.org/10.48550/arXiv.2303.16688",
language = "English",
publisher = "Arxiv",
type = "WorkingPaper",
institution = "Arxiv",

}

RIS

TY - UNPB

T1 - Model Checking Access Control Policies

T2 - A Case Study using Google Cloud IAM

AU - Gouglidis, Antonios

AU - Kagia, Anna

AU - Hu, Vincent C.

PY - 2023/3/29

Y1 - 2023/3/29

N2 - 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.

AB - 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.

KW - cs.CR

U2 - https://doi.org/10.48550/arXiv.2303.16688

DO - https://doi.org/10.48550/arXiv.2303.16688

M3 - Preprint

BT - Model Checking Access Control Policies

PB - Arxiv

ER -