AWS uses mathematics to validate Cloud WAN network segmentation

From network configurations to logical models

Organizations use wide-area networks to connect local networks across geographic regions, but they may also need to isolate resources within those networks. Development environments, for example, should remain separate from active websites. A segmentation error could allow traffic to reach an unintended part of a network or cross an organizational boundary.

Amazon Science says traditional validation has often involved sending packets through a network to map its behavior. The size and complexity of modern networks make it impractical to create a complete map this way, so organizations commonly test selected portions of a network instead. That sampling process does not exhaustively validate segmentation.

Tiros takes a static approach. For an AWS Cloud WAN deployment, specialized software collects route tables, attachments, and policy documents, then converts those configurations into logical propositions describing network behavior. Tiros analyzes the resulting model and derives the paths that can exist between network attachments and destination IP addresses.

Checking expected isolation across all modeled paths

The system compares the paths it derives with the segmentation specified by the network policy. If no path exists between segments that are supposed to be isolated, the validation succeeds. If the observed reachability differs from the expected segmentation, the system alerts an operator.

According to Amazon Science, Tiros can analyze the topology of a deployed AWS Cloud WAN network as often as every hour. The analysis provides a mathematical demonstration that the network’s topological description matches its isolation specifications, rather than testing only traffic that happens to pass through the network during a sampling period.

The method builds on Tiros’ earlier use in customer-facing services including Amazon Inspector, VPC Reachability Analyzer, and Network Access Analyzer. Those services focus on reachability, such as whether a valid sequence of requests can connect one network resource to another. Amazon’s stated insight is that determining reachable paths can also reveal when paths are absent between resources that should not communicate.

A safeguard for production and development environments

Amazon illustrates the approach with a company using Cloud WAN to connect resources in two regions, us-east-1 and us-west-2. Its policy defines separate production and development segments. VPC-prod-use1 and VPC-prod-usw2 belong to production, while VPC-dev-use1 belongs to development.

The example highlights a potential problem when VPC-prod-use1 and VPC-dev-use1 use the same address space, 10.0.0.0/16. If the VPCs were placed in the same segment, or if segmentation were misconfigured, a packet for that address space could have a nondeterministic destination. In practice, Amazon says, customer traffic could arrive at a development VPC instead of the production environment.

Tiros represents the configuration with rules and facts, then queries the model for assignments linking VPCs and IP addresses. If it finds no assignment in which a production VPC reaches a development VPC, or the reverse, the results show that the core network’s segmentation aligns with the policy.

What the approach means for AWS customers

The technique gives customers a way to validate segmentation without running separate reachability tests, according to Amazon Science. It is intended to provide assurance across all paths represented in the model, addressing a limitation of packet-based testing that can examine only selected traffic routes.

Amazon says the approach is not limited to Cloud WAN. Across AWS, automated reasoning is used to analyze system properties that are too large to test exhaustively. IAM Access Analyzer uses the Zelkova engine to help determine whether policies could grant access to resources from outside an account and to identify S3 buckets shared publicly or with other accounts. VPC Reachability Analyzer uses the same broader foundation to determine whether one network resource can reach another.

For network operators, the significance is a shift from testing sampled traffic to checking logical policies against modeled connectivity. The result depends on the configuration information represented in the model, but AWS presents Tiros as a way to repeatedly verify whether a deployed Cloud WAN topology continues to enforce its intended segmentation.