Evolving Verified Cloud Authorization

You must register and request HCSS Community Membership to view the slides and presentation video.

Abstract: Amazon Web Services (AWS) authorizes over 34 trillion requests per day [1]. AWS has a custom language for specifying access control policies and a corresponding authorization engine. For each request, the authorization engine determines whether access should be granted or denied based on the relevant policies. In this talk, we describe our experience verifying the authorization engine in the context of a large, actively developed code base where many developers are not familiar with formal methods. We use Dafny, a verification-aware programming language, to specify authorization at a high level, implement it efficiently, and prove properties of the algorithm. 

Authorization executes on a JVM, so we decided to compile the Dafny implementation to Java. To earn trust with developers, we insisted at the start that any generated code should be reviewable by anyone familiar with Java. Dafny’s built-in Java compiler does not generate readable code, so we wrote a custom compiler that generates idiomatic Java from our Dafny implementation. The Java code is reviewed in the same way as every other piece of code at Amazon. 

To manage the changes to the language and implementation, we are developing novel tools to do proofs that can relate two revisions of the same source code, a technique we call proof evolution. This allows us to prove, for example, that the interpretation of existing policies is unchanged by the addition of a new feature, which reduces the operational and security risk of authorization changes.

Sean McLaughlin is a principal applied scientist at AWS in Seattle. At Amazon he has worked on static analysis of software defined networks, verification of cryptographic protocols, and formal analysis of authorization.  He currently works on formal verification using Dafny, especially in the context of a quickly evolving code base, and idiomatic compilers. When not working, he likes spending time with his two kids and English Labrador.