KEYNOTE: Enabling Provable Security at Scale

Presented as part of the 2021 HCSS conference. 

ABSTRACT:

The cloud model can be viewed as a contract between customers and providers: customers program against the cloud model, and the cloud provider faithfully implements the model.  In this talk, we focus on the problem of access control. Many users are moving sensitive workloads to the cloud and require that their access control policies comply with their governance requirements and security best practices.  In this talk, I will present an overview of Zelkova, an SMT-based analysis engine, for verification of Amazon Web Services (AWS) access control policies that govern permissions across entire applications in the cloud. It uses traditional formal verification techniques such as language transformation and off-the-shelf SMT solvers. zelkova can be queried to explore the properties of policies e.g. whether some resource is “publicly” accessible, and is leveraged in features such as Amazon S3 Block Public Access, AWS Config Managed Rules, and Amazon Macie. Our experience shows that to leverage formal policy analysis users must have sufficient technical sophistication to realize the criteria important to them and be able to formalize the properties of interest as zelkova queries. In 2019, we launched a publicly available service IAM Access Analyzer that leverages Zelkova to automatically identify resources such as S3 buckets and IAM roles that are shared with an external entity. We help users understand whether their policy is correct, by abstracting the policy into a compact set of positive and declarative statements that precisely summarize who has access to a resource. Users can review the summary to decide whether the policy grants access according to their intentions.

Neha Rungta is a senior principal applied scientist in the Automated Reasoning Group with Amazon Web Services (AWS), working on formal verification techniques for cloud security. Prior to joining AWS, Neha was well-known for her work on symbolic execution, automated program analysis, and airspace modeling at the NASA Ames Research Center. She earned a PhD in computer science from Brigham Young University in 2009.