PV3 ⊧ TIROSchecks user-specified queries for AWS-based networks

Reachability analysis for AWS-based networks

Application domain/field

• Reachability analysis
• Cloud networks

Type of tool

Reachability checker

Expected input

• Model of the network, consisting of:
• Formal specification: formalizes the semantics of the AWS networking components, e.g. in which order a firewall applies rules, and how load balancers route traffic
• Snapshot: describes the topology and details of the network
• Query

Internals

Uses Soufflé, MonoSAT and Vampire. Should be able to answer queries such as "list all open paths from the Internet to any instance in the VPC (Virtual Private Cloud)"

Comments

Used by Amazon Web Services (AWS). It encodes the semantics of the entire AWS cloud network service stack. It has been made to scale well to networks of hundreds of thousands of instances, routers and firewall rules.