UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

Semantic-based Automated Reasoning for AWS Access Policies using SMT

Backes, J; Bolignano, P; Cook, B; Dodge, C; Gacek, A; Luckow, K; Rungta, N; ... Varming, C; + view all (2019) Semantic-based Automated Reasoning for AWS Access Policies using SMT. In: Proceedings of 2018 Formal Methods in Computer Aided Design (FMCAD). (pp. pp. 206-214). IEEE: Austin, TX, USA. Green open access

[thumbnail of Semantic-based Automated Reasoning for AWS Access Policies using SMT.pdf]
Preview
Text
Semantic-based Automated Reasoning for AWS Access Policies using SMT.pdf - Accepted Version

Download (352kB) | Preview

Abstract

Cloud computing provides on-demand access to IT resources via the Internet. Permissions for these resources are defined by expressive access control policies. This paper presents a formalization of the Amazon Web Services (AWS) policy language and a corresponding analysis tool, called ZELKOVA, for verifying policy properties. ZELKOVA encodes the semantics of policies into SMT, compares behaviors, and verifies properties. It provides users a sound mechanism to detect misconfigurations of their policies. ZELKOVA solves a PSPACE-complete problem and is invoked many millions of times daily.

Type: Proceedings paper
Title: Semantic-based Automated Reasoning for AWS Access Policies using SMT
Event: 2018 Formal Methods in Computer Aided Design (FMCAD)
ISBN-13: 9780983567882
Open access status: An open access version is available from UCL Discovery
DOI: 10.23919/FMCAD.2018.8602994
Publisher version: https://doi.org/10.23919/FMCAD.2018.8602994
Language: English
Additional information: This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions.
Keywords: Access control, Tools, Syntactics, Encoding, Semantics, Cloud computing
UCL classification: UCL
UCL > Provost and Vice Provost Offices > UCL BEAMS
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science
URI: https://discovery.ucl.ac.uk/id/eprint/10081411
Downloads since deposit
726Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item