- AWS's Tiros automated-reasoning tool can analyze the topology of a deployed AWS Cloud WAN network as often as every hour. It gives a mathematical demonstration that the network matches its isolation specifications, with no dynamic packet sampling.
- Tiros works from Cloud WAN route tables, attachments, and policy documents, which specialized software converts into logical propositions. Tiros then derives the reachable paths, and the system alerts an operator if reachability differs from the expected segmentation.
Corporations, banks, hospitals, and academic institutions all rely on wide-area networks (WANs) to connect their local networks across geographic regions. Within a WAN, however, it’s often necessary to isolate different computational resources from each other: for example, coding environments used to test new website features should remain separate from active websites.
Customers rely on such isolation — or segmentation — to help protect sensitive data; a single misconfiguration of segmentation rules could allow traffic to reach unintended parts of a network or allow data to cross organizational boundaries.
Historically, validating network segmentation has involved mapping the network by sending packets through it. The size and complexity of modern networks, however, make it impractical to build a complete map this way, so organizations instead rely on a sampling process that sends packets through only portions of the network. The result is that network segmentation is rarely validated exhaustively.
By using Tiros, Amazon Web Services’ automated-reasoning tool for analyzing network connectivity, we’re offering an alternative to dynamic sampling that is designed to validate segmentation across all modeled paths.
Previously, Tiros had been used in customer-facing services such as Amazon Inspector, VPC Reachability Analyzer, and Network Access Analyzer. These services focus on reachability, or determining whether some sequence of valid requests leads from one network resource to another. Our key insight is that if we can determine the reachable paths in a network, then we can also identify the absence of paths between particular resources.
Fundamentally, automated segmentation validation is a static process: it examines a network without relying on dynamic packet traffic. Using Tiros, we can analyze the topology of a deployed network as frequently as every hour. These analyses provide a mathematical demonstration that the topological description aligns with our isolation specifications.
Automated segmentation validation
In modern networking, a virtual network sits on top of the physical network of servers and wires and other components. Segmentation is achieved through logical rules and routing policies rather than physical isolation of network hardware.
We consider the case in which an Amazon Web Services (AWS) customer is using the AWS Cloud WAN service to configure and deploy a large organizational WAN. To validate network segmentation using Tiros, we first collect the customer’s Cloud WAN configuration from route tables, “attachments” (which are like a virtual cable within the network), and policy documents. Specialized software converts these configurations into logical propositions that describe network behavior. Now, we have a configuration that’s expressed logically, so that automated reasoning tools can analyze it.
Then we ask Tiros, “Which attachments can reach which attachments with which destination IPs?” Tiros generates the satisfying assignments it can derive from the network description, each of which corresponds to a path. Our system checks that no path exists between segments that the policy declares should be off limits from each other. If actual reachability matches the expected segmentation, the validation check succeeds; if they differ, the system alerts an operator.
Virtual private clouds and network predicates
Consider a global company that uses Cloud WAN to connect resources all over the world and manage a website for selling and supporting its products. When the company updates its website, it does so from a replica of the public-facing website inside the development environment within Cloud WAN. The production environment needs to be strictly contained, so that tests and changes not yet ready for deployment don’t reach the live website, which is maintained in the separate production environment. So the company’s software developers write a policy, or a collection of logical rules, that captures the need for this segmentation.
The policy defines two segments, production and development, across two regions, us-east-1 and us-west-2, as in the figure above. Attachment policies use tags to assign Virtual Private Clouds (VPCs, logically separated networks within larger networks) to various other network segments. In this policy, VPCs are tagged such that VPC-prod-use1 and VPC-prod-usw2 join the production segment and VPC-dev-use1 joins the development segment, as in the figure.
Observe, also, that in the figure, VPC-prod-use1 and VPC-dev-use1 are destinations within the same address space, 10.0.0.0/16. In this context, segmentation becomes critical; if the VPCs were deployed within the same segment, or segmentation was misconfigured, a packet destined for that address space would have a nondeterministic destination, VPC-prod-use1 or VPC-dev-use1. Practically speaking, such a misconfiguration could cause customer traffic to erroneously arrive in a development VPC.
Using Tiros, we take the core network configuration above and build a logical model of the network composed of rules (conditional predicates) and facts (unconditional predicates). Once the model is built, we can query Tiros for the instances of segmentation it derives for the attachments in the model.
When given predicates, facts, and a query, Tiros generates the assignments associated with each VPC and IP for which the query is provable within the model. If, for instance, Tiros finds no assignment where a production VPC reaches a development VPC, or a development VPC reaches a production VPC, then the results indicate that the core network’s segmentation aligns with the stated policy.
Future work
Segmentation validation demonstrates how automated reasoning can provide the kind of assurance that packet-based testing cannot. By encoding network configurations as logical propositions and using Tiros to explore the possible paths in the model, we can check segmentation against the stated policy rather than just sampling it. Customers do not need to run separate reachability tests.
This approach is not unique to Cloud WAN. Across AWS, automated reasoning is used to analyze properties of systems that are too large to test exhaustively. Using an engine called Zelkova, IAM Access Analyzer helps you identify whether a policy could grant access to a resource from outside your account and uses the same reasoning to help identify S3 buckets that are shared publicly or with other accounts. Similarly, VPC Reachability Analyzer helps determine whether one resource can reach another in your network. They all share the same foundation: translating configurations into logic and checking whether the properties you care about hold.
Research areas Dan DaCosta Dan is a senior applied scientist at Amazon.