一句话：提出 Block Public Access，用 SMT 与残差策略验证访问控制策略不授予公共访问，并已在 AWS 生产部署。
云服务数据高度敏感，访问由 DSL 编写的访问控制策略控制。DSL 表达力强，但误配置可能造成公开访问等安全问题。论文提出 Block Public Access，形式化定义 Trust Safety，刻画策略是否允许不受约束的公共访问；将策略编译为逻辑公式，其不可满足性可由 SMT 检查并保证 Trust Safety。由于 DSL 构造使该检查为 PSPACE 完全，难以应对云规模每秒数百万请求，作者利用策略结构计算仅涉及非可信访问的残差策略，使常见情况无需 SMT 即可语法验证。工具已集成到 AWS S3 授权系统并在生产中每日分析数百万策略，确认存储桶不会授予意外公共访问。
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.
@inproceedings{paperbot5862,
title = {Block public access: trust safety verification of access control policies},
author = {Malik Bouchet and Byron Cook and Bryant Cutler and Anna Druzkina and Andrew Gacek and Liana Hadarean and Ranjit Jhala and Brad Marshall and Dan Peebles and Neha Rungta and Cole Schlesinger and Chriss Stephens and Carsten Varming and Andy Warfield},
booktitle = {FSE},
year = {2020},
doi = {10.1145/3368089.3409728}
}