Reasoning about Stateful Network Behaviors
Network operators must ensure their networks meet intended traversal policies (e.g., host A can talk to host B, or inbound traffic to host C goes through a firewall and then a NAT). Violations of the policies may result in revenue loss, reputation damage, and security breaches. Today checking whether the intended policies are enforced correctly is stymied by two fundamental sources of complexity: the diversity and stateful nature of the behaviors of real networks. First, we need to account for vast diversity in both the control plane (e.g., different routing protocols and their interactions) and the data plane (e.g., routers, firewalls, and proxies) of the network. Second, we need to reason about a very large space of stateful behaviors in both the control plane (e.g., the current state being characterized by the route advertisements the routers have seen so far) and the data plane (e.g., a firewall’s current state with respect to a TCP session). Prior work on checking network policies is limited to a particular state of the network. Any attempt to reason about the behavior of the network across its state space is hindered by two fundamental challenges: (i) capturing the diversity of the control and data planes, and (ii) exploring the state space of the control and data planes in a scalable manner. This thesis argues for the feasibility of checking the correctness of realistic network policies by addressing the above challenges via two key insights. First, to combat the challenge of diversity, we design unifying abstractions that glue together different routing protocols in the control plane and diverse network appliances (e.g., firewalls, proxies) in the data plane. Second, to explore the state space of the network in a scalable manner, we build tractable models of the control and data planes (e.g., by decomposing logically independent tasks) and design domain-specific optimizations (e.g., by narrowing down the scope of search given the intended policies). Taken together, these two ideas enable systematic reasoning about the correctness of stateful data and control planes. We show the utility and performance of these techniques across a range of realistic settings.