Visible to the public Access Control Verification for Everyone

Amazon Web Services (AWS) recently launched IAM Access Analyzer, an automated reasoning service for auditing permissions to cloud resources. While all customers want increased security, few have the specialized skills required to formally specify and verify security properties. Customers who go down this road have to formally specify their intended security properties, check them against their policies, and then debug when properties fail to hold. Access Analyzer inverts this situation: it quickly and automatically discovers security properties and then asks customers which ones are intended. This eliminates the skill barrier and upfront time costs associated with traditional formal verification. As a result, everyone can have formally verified security properties and the confidence that comes with them.

Andrew Gacek is a Senior Applied Scientist in the Automated Reason Group at Amazon Web Services. Andrew designs services that use automated reasoning to help customers secure their applications and data. Previously, Andrew worked at Rockwell Collins, building formal verification tools for certification of safety critical avionics systems. Andrew holds a PhD in Computer Science from the University of Minnesota.


Creative Commons 2.5

Other available formats:

Access Control Verification for Everyone