Formal Reasoning about the Security of Amazon Web Services

This lecture was recorded: available in our gallery.

Abstract

Amazon Web Services (AWS) uses and develops tools based on formal verification to reason about the security of AWS itself, as well as the security of systems that customers build on AWS.  This talk will focus on how AWS services connect customers to logic-based techniques, as well as how AWS uses formal verification internally to provide higher assurance of its security.

Bio

Dr. Byron Cook is Director of Automated Reasoning at Amazon Web Services and Professor of Computer Science at University College London.  Prior to joining Amazon, Byron was known for his contributions to the Terminator/T2 termination prover,  BioModelAnalyzer, SLAM, and Microsoft’s Static Driver Verifier.