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

Block public access: Trust safety verification of access control policies

Bouchet, M; Cook, B; Cutler, B; Druzkina, A; Gacek, A; Hadarean, L; Jhala, R; ... Warfield, A; + view all (2020) Block public access: Trust safety verification of access control policies. In: ESEC/FSE 2020 - Proceedings of the 28th ACM Joint Meeting European Software Engineering Conference and Symposium on the Foundations of Software Engineering. (pp. pp. 281-291). Association for Computing Machinery (ACM): Virtual. Green open access

[thumbnail of 3368089.3409728.pdf]
Preview
Text
3368089.3409728.pdf - Published Version

Download (934kB) | Preview

Abstract

© 2020 Owner/Author. Data stored in cloud services is highly sensitive and so access to it is controlled via policies written in domain-specific languages (DSLs). The expressiveness of these DSLs provides users flexibility to cover a wide variety of uses cases, however, unintended misconfigurations can lead to potential security issues. We introduce Block Public Access, a tool that formally verifies policies to ensure that they only allow access to trusted principals, i.e. that they prohibit access to the general public. To this end, we formalize the notion of Trust Safety that formally characterizes whether or not a policy allows unconstrained (public) access. Next, we present a method to compile the policy down to a logical formula whose unsatisfiability can be (1) checked by SMT and (2) ensures Trust Safety. The constructs of the policy DSLs render unsatisfiability checking PSPACE-complete, which precludes verifying the millions of requests per second seen at cloud scale. Hence, we present an approach that leverages the structure of the policy DSL to compute a much smaller residual policy that corresponds only to untrusted accesses. Our approach allows Block Public Access to, in the common case, syntactically verify Trust Safety without having to query the SMT solver. We have implemented Block Public Access and present an evaluation showing how the above optimization yields a low-latency policy verifier that the S3 team at AWS has integrated into their authorization system, where it is currently in production, analyzing millions of policies everyday to ensure that client buckets do not grant unintended public access.

Type: Proceedings paper
Title: Block public access: Trust safety verification of access control policies
Event: ESEC/FSE '20: 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering
ISBN-13: 9781450370431
Open access status: An open access version is available from UCL Discovery
DOI: 10.1145/3368089.3409728
Publisher version: https://doi.org/10.1145/3368089.3409728
Language: English
Additional information: © 2020 Copyright held by the owner/author(s). https://creativecommons.org/licenses/by/4.0/
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/10167547
Downloads since deposit
7Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item