Forem: Cheshire Cat

Solving AWS Network Puzzles with Mathematics - Part 2

Cheshire Cat — Wed, 22 Jan 2025 17:22:38 +0000

Introduction

This article is the second post in my three-part series exploring mathematical approaches to analysing AWS networks.

Solving AWS Network Puzzles with Mathematics - Part 1
Solving AWS Network Puzzles with Mathematics - Part 2 (we are here)

As discussed in the previous instalment, network troubleshooting presents inherent challenges that cannot be overstated. Network and security configurations are diverse and multifaceted in cloud computing environments like AWS. Moreover, these configurations interact in complex ways to determine whether communication paths connect or disconnect. Many readers have likely found themselves caught between pressing tasks and uncooperative networks, leading to moments of genuine frustration.

This series aims to address the inherent complexity of networks, with particular emphasis on systematic and objective approaches that transcend individual experience or skill levels. In my previous article, I introduced VPC Reachability Analyzer as an automated solution for network troubleshooting challenges. In this second part, we shall shift our focus slightly to examine the core technology that powers this functionality.

At the heart of VPC Reachability Analyzer lies a powerful mathematical tool: SMT solvers.

SAT Solvers

To understand SMT solvers, we must first examine their foundational component: SAT solvers. "SAT" comes from "satisfiability," a concept central to computational logic.

Let us consider a propositional logic formula. Such a formula might take forms like P ∨ Q or ¬(P ∧ Q) ∨ R, where P, Q, and R represent propositional variables. For those familiar with programming languages, these propositional variables can be understood as analogous to boolean values in code.

Since P, Q, and R are boolean values, they can each be assumed true or false. Satisfiability (SAT) problems ask whether assigning appropriate values to these variables is possible so that the entire formula is evaluated as true.

When learning new concepts, examining concrete examples often proves illuminating. Consider the following formula:

(P ∨ Q) ∧ (P ∨ ¬Q) ∧ (¬P ∨ ¬Q)

What boolean values should we assign to P and Q to satisfy this formula? Let us reason through this step by step. We can deduce that at least one of P or Q must be true from P ∨ Q being true. Furthermore, ¬P ∨ ¬Q being true tells us that at least one of P or Q must be false. Finally, P ∨ ¬Q being true leads us to conclude that P must be true and Q must be false.

Let us explore another example. Consider this modified formula:

(P ∨ Q) ∧ (P ∨ ¬Q) ∧ (¬P ∨ ¬Q) ∧ (¬P ∨ Q)

This formula adds one more clause, (¬P ∨ Q), to our previous example. Notably, this modification leads to an interesting property: no matter how we assign truth values, the entire formula cannot be evaluated as true. In our previous formula, the only viable possibility was setting P to true and Q to false. However, the newly added clause (¬P ∨ Q) prohibits this combination.

Thus, we have observed the fundamental difference between these two formulae. The first formula is satisfiable, while the second is not. The satisfiability problem, at its core, is precisely the challenge of determining which category a given formula falls into.

SAT solvers are capable partners that automatically resolve these satisfiability problems. While we manually determined the values for P, Q, and R in our examples, such an approach becomes untenable when dealing with a hundred variables rather than just three. Finding the correct truth assignment (which might not even exist!) would be an unreasonable task for a manual calculation. Practical SAT solvers incorporate sophisticated optimisations, enabling them to solve even large-scale problems quickly.

Does this mean that SAT solvers can handle any computational problem? Not exactly. Despite their impressive computational capabilities, they are bound by a critical limitation: SAT solvers can only process propositional logic formulae. As we saw earlier with P, Q, and R, variables that assume boolean values are called propositional variables, and formulae containing only such variables are termed propositional logic formulae. To leverage a SAT solver for real-world problems, one must first express the problems in propositional logic.

However, this approach proves highly inefficient. As readers of this article should understand, our world is not constructed only of boolean variables. We regularly work with numerics, strings, and various other data structures. Representing conditions involving numbers or strings using only propositional logic results in practically impossible or, where possible, serious complications.

Let us consider another example. Suppose we have the following formula: variables x, y, and z are numeric. This example, therefore, extends beyond the realm of propositional logic:

(x < y + 2) ∧ (x = 2z + 10) ∧ (y + z ≥ 10)

This formula is indeed satisfiable. We can verify this by assigning values such as x = 12, y = 11, and z = 1. However, rewriting this using propositional logic leads to two alarming consequences.

First, we encounter explosive growth in the number of logical clauses. Even if we restrict our variables to values between 0 and 255, expressing just the portion x < y + 2 would result in an enormously long formula:

(x = 0 ∧ y = 0) ∨ (x = 0 ∧ y = 1) ∨ … ∨ (x = 0 ∧ y = 255) ∨ … (x = 1 ∧ y = 0) ∨ (x = 1 ∧ y = 2) ∨ … ∨ (x = 1 ∧ y = 255) ∨ …

Second, and perhaps more fundamentally, SAT solvers lack any genuine understanding of numerical properties, resulting in highly inefficient reasoning processes. For instance, when encountering an expression like x < x during processing, a SAT solver cannot arrive at this conclusion while we can immediately determine its unsatisfiability. In other words, SAT solvers lack the "knowledge" of numerical relationships we naturally grasp.

How, then, can we effectively harness the powerful automation capabilities of the solvers for real-world problems such as AWS network analysis? One answer lies in the SMT solvers, which we shall explore next.

SMT Solvers

SMT solvers can be considered SAT solvers enhanced with "knowledge." In addition to the core SAT-solving component, SMT solvers incorporate theory solvers specialised for specific domains. These theory solvers handle reasoning about integers, strings, bit vectors, and other specialised domains, while the SAT solver manages purely logical operations. The selection of appropriate theory solvers represents a crucial architectural decision determining the solver's capabilities and performance characteristics.

Consider our previous formula:

(x < y + 2) ∧ (x = 2z + 10) ∧ (y + z ≥ 10)

An SMT solver equipped with integer arithmetic "knows" about inequalities, enabling it to solve such formulae directly. Similarly, an SMT solver with string theory capabilities can determine the formula is unsatisfiable:

str ++ "b" = "a" ++ str

When analysing the number of “a”s at the beginning of each side, one can readily conclude that this equation cannot hold regardless of the value assigned to str.

We shall now explore how this intelligence is integrated into SAT solving, in other words, how SAT solvers and theory solvers collaborate. While actual SMT solvers employ various sophisticated optimisations beyond the scope of the simple overview, we shall examine a simplified sketch for educational purposes. This approach will allow us to follow the flow step by step and provide a clearer understanding of the fundamental principles at work.

Let us examine the following formula:

((x > 0) ∧ (y - 2z ≥ 0)) ∧ (¬(x > 0) ∨ (y = z)) ∧ (¬(x > 0) ∨ (z ≥ x))

As discussed, SAT solvers cannot directly handle integer arithmetic or inequalities. Conversely, arithmetic theory solvers cannot handle logical operators. To resolve this dilemma, we first transform this formula, which contains arithmetic operations, into pure propositional logic.

Assume the following substitutions:

P := x > 0
Q := y - 2z ≥ 0
R := y = z
S := z >= x

With these substitutions, we can view the original formula as the following propositional formula:

(P ∨ Q) ∧ (¬P ∨ R) ∧ (¬P ∨ S)

This transformation process is known as boolean abstraction. It is crucial to note that the transformed formula contains less information than the original arithmetic-containing formula. Consequently, while the propositional formula may be satisfiable, this does not guarantee the satisfiability of the original formula. However, if the propositional formula proves unsatisfiable, we can definitively conclude that the original formula must also be unsatisfiable.

Having transformed the formula into propositional logic, we can now apply our SAT solver. The solver determines that this propositional formula is indeed satisfiable, with one possible assignment being:

P: true, Q: true, R: true, S: true

Our next step involves translating these propositional variables back to their original arithmetic expressions, resulting in the following arithmetic constraints:

x > 0
y - 2z ≥ 0
y = z
z ≥ x

Revealing boolean-abstracted conditions to their original form is called refinement. While these conditions might appear identical to our starting point, closer examination reveals a crucial difference. For instance, where the original formula allowed the condition corresponding to P to be either true or false, we have now narrowed it down to require that x > 0 be true specifically.

When we apply refinement to our constraints, they are evaluated by the theory solver. Unfortunately, this set of conditions proves unsatisfiable: no values exist for x, y, and z that could simultaneously satisfy all constraints. What does this tell us? It reveals that our assignment of "P: true, Q: true, R: true, S: true" is impossible. This insight emerges from the theory solver providing information that the SAT solver alone could not discover. This demonstrates what we mean when we say boolean abstraction reduces the info.

Having discovered that "P: true, Q: true, R: true, S: true" is impossible, we can add the negation of this condition to our propositional formula and resubmit it to the SAT solver. This process of feeding back discovered conditions is known as learning. Our new formula, with the additional term representing our learned constraint, becomes:

(P ∨ Q) ∧ (¬P ∨ R) ∧ (¬P ∨ S) ∧ ¬(P ∧ Q ∧ R ∧ S)

This time, the SAT solver discovers a new assignment:

P: false, Q: true, R: true, S: true

When we apply refinement again to convert these assignments back to arithmetic expressions, we obtain the following constraints for our theory solver. Note that since P (corresponding to x > 0) is assigned false, we now have the constraint x ≤ 0:

x ≤ 0
y - 2z ≥ 0
y = z
z ≥ x

And here comes the breakthrough: these constraints are indeed satisfiable! The SMT solver would likely report a solution such as x = 0, y = 0, and z = 0.

It's noteworthy that actual SMT solvers employ far more sophisticated mechanisms than this simplified explanation suggests. They incorporate various optimisations for enhanced performance.
For instance, we added the negation of the entire constraint set in our learning example. Still, a more efficient approach would be to identify and learn from minimal subsets of constraints that cause contradictions.

Another well-known optimisation technique is online integration, where the solver consults the theory solver for partial constraint evaluation before fully determining all propositional variable assignments. This approach differs from our example, where we waited until all assignments were complete before performing refinement.

Conclusion

In this article, we have explored the theoretical foundations underlying VPC Reachability Analyzer, which we introduced in our previous post. Specifically, we have examined the mechanisms and capabilities of SAT and SMT solvers. Through a simplified yet concrete example, we have traced the step-by-step process of how a SAT solver and a theory solver collaborate within an SMT solver, providing a detailed trace of its action flow.

In our final article of this series, we shall dive into the core engine of VPC Reachability Analyzer itself. We will explore how this powerful tool elegantly applies SMT solver technology to resolve the typical problems of AWS network troubleshooting. This last piece will combine all the concepts discussed throughout this series, demonstrating how theoretical foundations translate into practical solutions for everyday networking challenges.

Solving AWS Network Puzzles with Mathematics - Part 1

Cheshire Cat — Thu, 28 Mar 2024 20:05:33 +0000

Introduction

As engineers utilising AWS, many readers have likely encountered network issues at some point. These situations may include instances where expected communication between EC2 Instances fails to reach its destination or, conversely, when communication that should be blocked succeeds in reaching its destination. In such cases, one may be at a loss regarding modifying the numerous, complexly related Security Groups. In these moments, it is an undeniable fact that an expert's advanced knowledge and experience can be invaluable in solving the puzzle. However, are these the only tools at our disposal?

This article explores a solution that relies on established mathematical theories, an additional thought process beyond one's brain. Specifically, we aim to understand the research paper "Reachability Analysis for AWS-Based Networks" published by Backes et al. in 2019 and the subsequently implemented feature, VPC Reachability Analyzer and VPC Network Access Analyzer.

However, this paper is highly specialised, and understanding it without prior knowledge can be challenging. This series of articles will be divided into three parts to provide a comprehensive explanation.

Solving AWS Network Puzzles with Mathematics - Part 1 (we are here)
Solving AWS Network Puzzles with Mathematics - Part 2

In this initial article, we will examine a concrete example of a network configuration on AWS and explore the functionality and positioning of VPC Reachability Analyzer.

Configuration of a Sample Network

Let's consider a compact, uncomplicated network that is robust enough to demonstrate the capabilities of VPC Reachability. The diagram below illustrates this network architecture.

Examining the diagram shows that within the VPC are two Subnets labelled X and Y, hosting EC2 Instances A, B, and C. Additionally, Security Groups aiming to allow communication through port 22 have been attached to the Instances.

Now, let's ask our readers an initial question: Is SSH communication from Instance A to C possible? The answer is clearly yes. The settings of Security Group 1 make this possible. On the other hand, it should be equally clear from the diagram that SSH communication from Instances B to C will be blocked by the misconfigured Security Group 2, limiting the destination to the local. Moreover, assigning a public IP address allows Instance C to access the Internet; it potentially violates your security compliance.

This might seem like a simple matter. However, is network connectivity always straightforward? Certainly not. In real-world production environments, many EC2 Instances and other computational resources are closely interconnected with Security Groups and Route Tables involving routing to multiple networks. In such complex production environments, determining which Instances can communicate with others and which cannot is a task full of complexity.

So, what are the potential consequences of this complexity? You carefully review the infrastructure, defined using CDK or Terraform, on GitHub. It looks perfect. You go ahead and deploy. At this point, you realise that your carefully deployed network isn't working as expected.

Dual Approaches to Troubleshooting

When faced with a problem, two main troubleshooting methods are available to us.

The first approach involves actively sending packets and then checking connectivity. This is a well-established technique that predates our move to the cloud. From the essential ping, traceroute, and telnet commands to the more versatile netcat utility, an experienced infrastructure engineer's toolbox is filled with various tools. Alternatively, if the issue is within a database, one may investigate the application's behaviour and logs to determine the root cause.

The second approach involves forgoing the sending of actual packets and carefully examining the configuration to identify the root cause. By logging into the AWS Management Console and navigating through numerous pages, combining the various pieces of information in one's mind, one may ultimately identify the incorrect configuration that caused the problem. This is an impressive accomplishment, a testament to the skill of an experienced engineer.

The two approaches described above are, in a way, opposite. One involves active trial and error, while the other relies on the role of an armchair detective to identify the cause. However, a key characteristic unites these two methods: they are both stressful. A single misplaced entry in a Route Table with many configurations closely intertwined can block communication. Few engineers would voluntarily take on the task of solving this puzzle.

Power of VPC Reachability Analyzer

Who, then, shall unravel this enigma if not you? The answer lies in the VPC Reachability Analyzer. This powerful tool can automatically resolve issues related to network behaviour examples without requiring human intervention.

The role of humans is limited to simply specifying the conditions for communication. For example, one might define the source and destination EC2 Instances, protocol, and port number. At the cost of a small amount of time and usage fees, the Analyzer will provide a resolution, determining whether the communication is possible.

What is particularly interesting is that during this operation, the Analyzer does not send any packets. Instead, it examines the configuration items rather than the actual communication results. Like an experienced engineer, the Analyzer possesses "knowledge" about the network.

This leads to another significant advantage. If the Analyzer were to assess reachability by sending packets in a way similar to the traceroute command, the communication would be unable to proceed beyond the point where a component with a discontinuous configuration is encountered, thus failing to obtain information about the entire communication path.

However, in reality, the Analyzer analyses the "meaning" of the configurations. As a result, it can provide a comprehensive answer, including which configurations are problematic and require fixing. This becomes clear when examining the actual results screen presented below.

Upon initial inspection of the results, one is immediately drawn to the red icon, accompanied by the concerning message: "None of the egress rules in the following security groups apply." This troubling finding reveals the root cause of the SSH connection's failure, originating from the previously discussed misconfiguration of the Security Group. Moreover, it is particularly significant that the Analyzer displays the entire path from the source to the destination, clearly identifying the point of misconfiguration. This clear visualisation offers valuable guidance on resolving the network connectivity problem.

Syntax, Rules and Semantics

As previously explained, VPC Reachability Analyzer represents a verification paradigm that understands the inherent "meaning" of the configurations. When aiming to verify infrastructure as code, one can divide the verification levels into three tiers.

The first tier relates to syntactic verification, representing the most basic level. Imagine a scenario where you define your infrastructure using CloudFormation templates. In this context, syntactic verification is equivalent to examining the YAML file structure's compliance with the specified schema. As syntactic errors are directly related to the failure of the deployment itself, the necessity of this verification stands as an undeniable prerequisite. However, as previously noted, it is not a sufficient condition. The deployed resources operate according to your definitions rather than your intentions.

The second tier includes rule-based verification. One of the most typical rule-based verifications in the networking domain is the prohibition of access from 0.0.0.0/0. This rule, which comes pre-configured in AWS Trusted Advisor, denies exposure to the Internet. However, it is simply an explicit formulation of the knowledge that "allowing 0.0.0.0/0 is equivalent to granting access from the Internet."

The third and highest tier of verification under consideration is semantic verification. At this level, by providing the configurations as input, one can perform a verification that considers the "meaning" of how these configurations will manifest their effects. Imagine a scenario involving numerous components, where the interaction of their respective rules ultimately determines the network's reachability. In semantic verification, the need for individual judgments is eliminated by proactively formalising the mutual influence of rules, enabling the verification to determine whether the desired outcome will be achieved as the final result.

For the readers who have read this article thus far, it will be clear that this semantic verification is the distinguishing feature of VPC Reachability Analyzer. It is a decisive advantage for us engineers who are constantly challenged by network puzzles.

Conclusion

In this article, we have presented the challenges of network troubleshooting on AWS and introduced the capabilities of VPC Reachability Analyzer as a solution. Moreover, we have defined three tiers of verification for codified infrastructure, positioning Reachability Analyzer as the third tier enabling semantic verification.

In the subsequent article, we shall address how VPC Reachability Analyzer performs semantic verification, or in other words, what mechanisms it employs to comprehend the "meaning" of configurations. Specifically, we will introduce the foundational technologies of SAT and SMT solvers and elucidate their operating principles.

Appendix

You can try out VPC Reachability Analyzer and VPC Network Access Analyzer using the provided CloudFormation template.

Please note that I cannot be held responsible for any issues using this template. In particular, be aware that this template will launch actual EC2 instances, albeit small ones, and that both Analyzers incur costs (especially Reachability Analyzer, which is expensive at 0.1 USD per execution).

---
Description: 'Demo for VPC Analyzers'
AWSTemplateFormatVersion: 2010-09-09

Mappings:
  RegionMap:
    ap-northeast-1:
      execution: ami-02892a4ea9bfa2192

Resources:
  VPC:
    Type: AWS::EC2::VPC
    Properties:
      CidrBlock: 172.0.0.0/16

  InternetGateway:
    Type: AWS::EC2::InternetGateway

  InternetGatewayAttachement:
    Type: AWS::EC2::VPCGatewayAttachment
    Properties:
      InternetGatewayId: !Ref InternetGateway
      VpcId: !Ref VPC

  SubnetX:
    Type: AWS::EC2::Subnet
    Properties:
      VpcId: !Ref VPC
      CidrBlock: 172.0.1.0/24

  SubnetY:
    Type: AWS::EC2::Subnet
    DependsOn: InternetGateway
    Properties:
      VpcId: !Ref VPC
      CidrBlock: 172.0.2.0/24
      MapPublicIpOnLaunch: true

  PublicRouteTable:
    Type: AWS::EC2::RouteTable
    Properties:
      VpcId: !Ref VPC

  PublicRouteTableAssociation:
    Type: AWS::EC2::SubnetRouteTableAssociation
    Properties:
      RouteTableId: !Ref PublicRouteTable
      SubnetId: !Ref SubnetY

  PublicRoute:
    Type: AWS::EC2::Route
    Properties:
      RouteTableId: !Ref PublicRouteTable
      GatewayId: !Ref InternetGateway
      DestinationCidrBlock: 0.0.0.0/0

  SecurityGroup1:
    Type: AWS::EC2::SecurityGroup
    Properties:
      GroupDescription: 'Sample SG 1'
      VpcId: !Ref VPC
      SecurityGroupIngress:
        - CidrIp: !GetAtt VPC.CidrBlock
          IpProtocol: 'tcp'
          FromPort: 22
          ToPort: 22
      SecurityGroupEgress:
        - CidrIp: 0.0.0.0/0
          IpProtocol: '-1'

  SecurityGroup2:
    Type: AWS::EC2::SecurityGroup
    Properties:
      GroupDescription: 'Sample SG 2'
      VpcId: !Ref VPC
      SecurityGroupIngress:
        - CidrIp: !GetAtt VPC.CidrBlock
          IpProtocol: 'tcp'
          FromPort: 22
          ToPort: 22
      SecurityGroupEgress:
        - CidrIp: 127.0.0.1/32
          IpProtocol: '-1'

  InstanceA:
    Type: AWS::EC2::Instance
    Properties:
      ImageId:
        Fn::FindInMap:
          - RegionMap
          - !Ref AWS::Region
          - execution
      InstanceType: 't3.nano'
      SubnetId: !Ref SubnetX
      SecurityGroupIds:
        - !Ref SecurityGroup1
      Tags:
        - Key: Name
          Value: InstanceA

  InstanceB:
    Type: AWS::EC2::Instance
    Properties:
      ImageId:
        Fn::FindInMap:
          - RegionMap
          - !Ref AWS::Region
          - execution
      InstanceType: 't3.nano'
      SubnetId: !Ref SubnetX
      SecurityGroupIds:
        - !Ref SecurityGroup2
      Tags:
        - Key: Name
          Value: InstanceB

  InstanceC:
    Type: AWS::EC2::Instance
    Properties:
      ImageId:
        Fn::FindInMap:
          - RegionMap
          - !Ref AWS::Region
          - execution
      InstanceType: 't3.nano'
      SubnetId: !Ref SubnetY
      SecurityGroupIds:
        - !Ref SecurityGroup1
      Tags:
        - Key: Name
          Value: InstanceC

  ReachablePath:
    Type: AWS::EC2::NetworkInsightsPath
    Properties:
      Source: !Ref InstanceA
      Destination: !Ref InstanceC
      DestinationPort: 22
      Protocol: tcp
      Tags:
        - Key: Name
          Value: 'Reachable Path'

  BlockedPath:
    Type: AWS::EC2::NetworkInsightsPath
    Properties:
      Source: !Ref InstanceB
      Destination: !Ref InstanceC
      DestinationPort: 22
      Protocol: tcp
      Tags:
        - Key: Name
          Value: 'Blocked Path'

  AccessToInternet:
    Type: AWS::EC2::NetworkInsightsAccessScope
    Properties:
      MatchPaths:
        - Destination:
            ResourceStatement:
              ResourceTypes:
                - AWS::EC2::InternetGateway
      Tags:
        - Key: Name
          Value: 'All Access To Internet'