Title: The Cloud Model – Enabling Provable Security at Scale

Speaker: Neha Rungta

Affiliation: Amazon

Data and location: Friday, March 15, 12:30 – 1:30pm; Wozniak Lounge (430 Soda Hall)

Abstract: Cloud computing is the on-demand delivery of IT resources through a common services platform.  Businesses of all sizes are migrating their IT infrastructure to the cloud, both to reduce costs and increase agility for deploying new services and features. The cloud provides a precise model of resource configuration, communication, coordination, and storage.  It enables an ease of formalization and the verification technologies built for this model are applicable to millions of customers.

The programming model for cloud computing is similar in many ways to approaches seen in traditional model-driven design. 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 customers are moving sensitive workloads to the cloud and require that their access control policies comply with their governance requirements and security best practices.  We present the use 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. We verify various properties about access control at scale. These access control checks are integrated into various parts of the software development life cycle and can be leveraged for preventative (CI/CD pipeline, compliance), detective (audit, health monitoring), and reactive (alarming, remediation) controls. We describe how the infrastructure provided by the cloud enables ease of integration.

Bio: Dr. Neha Rungta is a Principal Engineer in the Automated Reasoning Group with Amazon Web Services (AWS) working on formal verification techniques for cloud security. Prior to joining AWS, Neha is known for her work on symbolic execution, automated program analysis, and airspace modeling at NASA Ames. She graduated with a PhD in Computer Science from BYU in 2009.