Presented as part of the 2019 HCSS conference.

John Backes, Pauline Bolignano, Byron Cook, Catherine Dodge, Andrew Gacek, Rustan Leino, Kasper Luckow, Neha Rungta, Oksana Tkachuk and Carsten Varming

Cloud computing provides on-demand access to IT resources via the Internet. In Amazon Web Services (AWS), access to these resources is controlled by policies which limit access based on who, what, when, and how. In this talk we describe Zelkova, a semantic analysis tool for AWS policies. Zelkova can determine if policies are misconfigured, overly permissive, or in violation of corporate governance rules. Customers can use Zelkova to prevent creation of incorrect policies or to audit existing policies for compliance. It is also the basis for the recently launched S3 Block Public Access feature which prevents users from misconfiguring their S3 buckets and causing unintentional world access. Zelkova provides a semantics for AWS policies via translation into the SMT theories of strings, regular expressions, bit vectors, and integers. Zelkova then uses several SMT solvers, including Z3 and CVC4, to solve these constraints.

Andrew Gacek is a Senior Applied Scientist in the Automated Reasoning Group at Amazon Web Services. Previously he worked in the Trusted Systems group of Rockwell Collins. He earned his Ph.D. in Computer Science from the University of Minnesota.