Formally verified AWS authorization

Industrial Problems Seminar

Sean McLaughlin (Amazon Web Services)

Abstract:

Amazon Web Services (AWS) is a cloud-computing service. Our APIs are called over a billion times per second world-wide. Each of those calls is authorized; an algorithm decides whether the call should be allowed based on a set of authorization policies.

Earlier this year, my team announced that we formally verified our authorization algorithm. In this talk, I'll describe the journey of the multi-year project from conception to deployment, and highlight lessons we learned applying science at scale.