Tiros: Reachability analysis for AWS-based Networks Using Automated Theorem Proving

Presented as part of the 2019 HCSS conference.

S. Bayless, B. Cook, C. Dodge, A. Gacek, A.J. Hu, T. Kahsai, B. Kocik, E. Kotelnikov, J. Kukovec, S. McLaughlin, J. Reed, N. Rungta, J. Sizemore, M. Stalzer, P. Srinivasan, P. Subotic, C. Varming, B. Whaley, Y. Wu

Cloud computing provides on-demand access to IT resources via the Internet. In Amazon Web Services (AWS), virtual machines and cloud-based resources are connected together by customers using a rich mixture of over 50 networking-based concepts, e.g. elastic network interfaces, elastic load balancers, and virtual private clouds. In this talk we describe an analysis tool, called Amazon Tiros, which uses automated theorem proving to implement semantic-level reachability analysis for complex virtual networks constructed by AWS customers using AWS APIs. Tiros is the basis of a new feature in the security product Amazon Inspector. Tiros is also is also the primary component of new internal processes for establishing and maintaining FedRAMP compliance. Tiros solves complex networking questions tens of thousands of times daily. In this lecture we will describe Tiros's impact both within Amazon and also for our customers. Tiros is capable of using up to three possible solvers, each which use radically different technologies: MonoSAT, Souffle and, or Vampire. In the lecture we will also compare/contrast these underlying solvers for this application, as well as discuss lessons learned from operating the three solvers at industrial scale.

Note to reviewers: for publicly available information on Tiros, see

• https://aws.amazon.com/blogs/security/amazon-inspector-assess-network-exposure-ec2-instances-aws-network-reachability-assessments/
• https://www.wired.com/story/aws-cloud-security-tools-leaks/
• https://www.youtube.com/watch?v=JfjLKBO27nw
• https://aws.amazon.com/inspector/

John Backes is a Software Development Engineer on the Amazon Inspector service team at Amazon Web Services (AWS). He earned his PhD from the Department of Electrical and Computer Engineering at the University of Minnesota in 2013. Prior to joining AWS he was a Senior Research Scientists at Rockwell Collins. There he was the principle developer of AGREE, a compositional verification tool for AADL models. He was a member of the air vehicle team in DARPA's High Assurance Cyber Military Systems program. He has also been a performer on projects funded by NASA, AFRL, and the Army. At AWS he is the lead developer for the Tiros service, which performs semantic analysis of Virtual Private Cloud networks. His research interests include SMT-Solving, Model Checking, Formalization of Requirements, and Cloud Computing.