Provable Security and Automated Reasoning at Amazon

How do you know your software always does what it should? Are your access control policies too permissive? Will the communication protocol you use always keep your information safe and private? At Amazon Web Services, we have been steadily growing the use of *automated reasoning* (AR) techniques to *prove* that critical programs, policies, and protocols are correct and secure for all possible inputs. Such proofs give us confidence beyond that gained with testing or code reviews. When full proof is not feasible, we use a variety of other ideas and techniques drawn from the programming languages and formal methods research communities, such as static analysis, model checking, and differential and property-based random testing. The Automated Reasoning Group (ARG) began about eight years ago with just a few researchers. Today it comprises more than 100 scientists and many more engineers besides, and offers internships to both grad and undergrad students (we had more than 50 in my Org last year). In this talk I'll tell you about ARG, some ongoing efforts, and how you can get involved.