I describe the use of formal verification tools within Amazon Web Services to further ensure the security of its customers. We discuss some accomplishments, describe some of the challenges of operationalizing proof, muse on lessons learned, and outline some ideas for future research.
Byron Cook leads AWS Security’s Automated Reasoning Group which develops and applies constraint/logic based automated tools for proving the correctness of software, network configurations, and policies. Prior to joining AWS, Byron was for 10 years a researcher at Microsoft Research, where he worked in the areas of functional programming, hardware modeling and design, SAT-solving, symbolic model checking for finite-state systems, decision procedures, automatic program verification and analysis, and the analysis of biological systems. Byron’s research in automatic program verification has gained significant recognition (e.g. a substantial publication record, numerous keynote speaker invitations, and press hits in Scientific American, Science, Vogue, Financial Times, Economist, and Wired). Byron is particularly well known for his work on automatic methods for proving program termination, notably as part of the Terminator termination prover. This work represented a breakthrough, challenging the prevailing opinion in computer science that automatic termination proving is impossible. Byron is also well known for his contributions to Microsoft's SLAM project, which is often credited as a catalyst for the revival of automatic program verification research.