Bouchet, M; Cook, B; Cutler, B; Druzkina, A; Gacek, A; Hadarean, L; Jhala, R; ... Warfield, A; + view all Bouchet, M; Cook, B; Cutler, B; Druzkina, A; Gacek, A; Hadarean, L; Jhala, R; Marshall, B; Peebles, D; Rungta, N; Schlesinger, C; Stephens, C; Varming, C; Warfield, A; - view fewer (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.

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.

Download activity - last month

Export as JSONCSVXML

Download activity - last 12 months

Export as XMLCSVJSON

Downloads by country - last 12 months

Export as JSONCSVXML

Archive Staff Only

View Item