Speaker

Lucas Wagner

Abstract

In this talk you will learn how AWS uses formal methods to provide proof-based assurances for the security-critical authorization engine used in AWS’s Identity and Access Management (IAM) service. IAM allows customers to write access control policies that define fine-grained permissions to resources in their account. Incoming requests to AWS, 1B per second, are compared to these policies at runtime to determine if the request should be allowed or denied. This talk will cover how we applied formal methods at scale to successfully launch a new, 65% faster authorization engine, that behaves exactly the same as its predecessor.

Bio

Lucas Wagner is an Sr. Applied Science Manager at AWS with 20 years of experience applying formal methods in industry. Previously he was a Senior Principal Researcher at Collins Aerospace. He graduated from the University of Iowa in December of 2001 from the College of Engineering.