One-click Automated Reasoning in Amazon Web Services
Presented as part of the 2020 HCSS conference.
|
Amazon Web Services (AWS) recently launched IAM Access Analyzer, an automated reasoning service for auditing permissions to cloud resources. In this talk, we share the journey of bringing this formal methods technology to market. This includes wrestling with notions of correctness, getting users to specify correctness, and rethinking what correctness means. The result is a service based on formal methods yet accessible to everyday users.
Access Analyzer is built on top of Zelkova, an SMT-based analysis engine for AWS access control policies. The breakthrough in Access Analyzer is using predicate abstraction to provide a sound, precise, and compact summary of an access control policy. This summary enables compositional reasoning properties that are not possible of policies written in the underlying policy language. |
Andrew Gacek is a Senior Applied Scientist at Amazon Web Services (AWS). Over the last two years, Andrew has developed techniques to apply automated reasoning to the identity and access control domain. Prior to AWS, Andrew spent seven years as an industrial logician in the Trusted Systems group at Rockwell Collins. There, Andrew applied automated reasoning to the development and verification of safety critical flight control systems. Andrew holds a PhD in Computer Science from the University of Minnesota.