Automated Reasoning at Cloud Scale and the Business of Proof

Amazon Web Services (AWS) is a cloud computing services provider that has made significant investments in automated reasoning to check the correctness of its internal systems and to provide assurances to customers. We are using proof engines called SAT and SMT solvers more than one billion times a day, both for real-time queries in customer security (checking security policies and verifying network protections), and also for large queries involving code and hardware reasoning that are at the limits of what can be feasibly solved by current solvers. Reaching this scale requires that we consistently focus on our customers and provide measurable improvements for existing customer problems.  It also requires careful examination of the problems to be solved and a clear focus on operations to ensure our analyses are consistently trustworthy and performant. I will discuss these aspects and, more generally, steps to make automated reasoning successful in a commercial organization.

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 led development of simulation,translation, testing, and formal analysis tools for C, Rust, and Model-Based Development languages including Simulink, Stateflow, SCADE, and RSML-e, and has published 90 peer-reviewed articles on these topics. Dr. Whalen has led successful formal verification projects on foundational Amazon C libraries and 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”, looking at how to create proof engines that can cost-effectively scale to larger and more complex problems than are handled by current tools. He is also involved with outreach, helping developers and business customers apply verification tools to improve their team’s quality, velocity, and innovation.