This talk will focus on the development and use of formal verification tools within Amazon Web Services (AWS) to increase the security assurance of its cloud infrastructure and to help customers secure themselves. The talk will also touch on some remaining challenges that could inspire future research in the community.
Byron Cook is Professor of Computer Science at University College London (UCL) and Director of Automated Reasoning at Amazon Web Services. Byron is the founder and leader of Amazon’s Automated Reasoning Group (ARG). Previous to his work at AWS, Byron developed the Terminator termination prover, as well as Windows Static Driver Verifier.