Colloquium: Reasoning About the Security of AWS

November 4, 2019 - 11:15am to 12:15pm
Michael Whalen
3-180 Keller Hall
Mats Heimdahl
Abstract: Amazon is applying formal methods at scale to help secure the AWS cloud.  This commitment spans the gamut between higher-order proofs for optimized algorithms for cryptography to code-level verification of critical pieces of AWS architecture to specialized verification tools to ensure that users' network configurations and security policies are properly permissive. In this talk, I talk about why Amazon is applying formal reasoning, where Amazon is applying formal reasoning, and some open challenges in applying formal reasoning at "cloud scale". Finally, I will briefly discuss how we hope to collaborate with faculty and students to dramatically improve the scale and applicability of formal methods.
Bio: Dr. Michael Whalen is a Principal Applied Scientist at Amazon Web Services and the former Director of the University of Minnesota Software Engineering Center.  Dr. Whalen is interested in formal analysis, language translation, testing, and requirements engineering.  He has developed simulation, translation, testing, and formal analysis tools for Model-Based Development languages including Simulink, Stateflow, SCADE, and RSML-e, and has published more than 90 papers on these topics.  He has led successful formal verification projects on large industrial avionics models, including secure autonomous vehicles (DARPA HACMS project), pilots’ displays (Rockwell-Collins ADGS-2100 Window Manager), redundancy management and control allocation (AFRL CerTA FCS program) and autoland (AFRL CerTA CPD program).  He is currently working on formal verification at “cloud scale”, part of a team building tools that get used millions of times daily to help secure the AWS cloud.  He is working on improving the scalability of formal verification and extracting information from proofs to satisfy compliance and certification requirements.