Welcome back. We're starting a module on verification. The motivation behind verification is to determine whether the network is doing the right thing. In this module, we'll explore various techniques for verification, such as the verification of the configuration which was possible before software defined networking. We'll then look at Control Plane Verification and Data Plane Verification. Let's start by looking at Configuration Verification. What are the motivations behind verification is that figuring out the answers to even very simple questions turns out to be very difficult. Answering questions such as. What are all the packets from A that can reach B? What will happen if I remove an entry from a firewall? Is a group of hosts sufficiently isolated from another group of hosts? Are there loops, and what is the cause for poor network performance? All of these questions are relatively simple, but are surprisingly difficult to answer in today's networks. In conventional networks, the configuration of the network defines the behavior. Network configuration provides flexibility for realizing operational goals. It controls various aspects of behavior, such as how traffic enters and leaves the network, which neighboring networks can send traffic, and how routers within a network learn routes. Configuration offers a considerable amount of flexibility, but that flexibility also leads to complexity that makes the network hard to configure and debug. Now, the most important goal for any network should be correctness, and unfortunately mistakes happen. Mistakes occur because configuration is inherently difficult. Network operators can make mistakes. There are complex policies, and additionally, configuration can be distributed across hundreds to thousands of routers in the network. Often, individual components in a network are independently configured. Which can result in unintended policy interactions. In today's networks, verification doesn't really exist. A network operator can tweak a configuration and observe the effects. But this is a rather unacceptable programming environment. If an operator makes a mistake tweaking the configuration, downtime can result. Worse yet, if an operator makes a mistake, it might only become apparent much later. For example, if a link fails and a backup is misconfigured. Ultimately what we'd like to have, is a correctness specification and constraints for Internet routing. Rcc is a static configuration analysis tool for fault detection. It's been used by network operators, including those in large backbone networks. We released rcc about ten years ago, and performed analysis of real world network configurations from 17 different autonomous systems at the time, and found errors in every one of them. Here's a very high level overview of how rcc works. We start with a correctness specification. We then map that correctness specification, with a set of constraints that can be tested against an intermediate representation of distributed router configurations, and then produce a list of faults. It should be apparent from this high level architecture, that producing a set of faults is actually extremely challenging. First, we must parse the distributed router configurations, to come up with some intermediate representation. We then must develop a model to essentially, indirectly infer the behavior of the network. The constraints that we express against that model, are ultimately constraints on the low level router configurations. Unlike what is possible with STN, these constraints must be expressed in terms of low level router configurations. As opposed to higher level policies or properties of the network. There are many challenges in realizing such a system. Such as defining a correctness specification, deriving verifiable constraints from that specification, and analyzing complex, low-level distributed configuration. The way that rcc breaks this problem down, is to factor routing configuration into three counterparts. One is ranking or route selection. A second is dissemination, or internal route advertisement. And a third is filter, which controls how an AS advertises these routes to neighbors. Factoring routing configuration into these three sub problems makes it easier to express constraints on each aspect of routing. For each aspect of routing configuration, we can then ask questions about correctness. We start with a high level specification of what it means for a routing protocol to be correct. One aspect of correctness is called path visibility. Which says that, if every router learns a route, for every usable path, then path visibility is satisfied. A usable path is defined as a path that reaches the destination, and corresponds to the path that packets take, when using that route. The path should also conform, to policies of the routers on that path. In other words, if a packet takes a path to a destination, it should not traverse a router that has a policy that drops that packet. Possible faults with path visibility in the dissemination part of configuration, include partitions in the BGP session-level graph that disseminates routes inside an AS. Possible path visibility faults for filtering, include filtering routes for prefixes that correspond to useable paths. An example where path visibility can be violated in today's interdomain routing system, is internal BGP. The default way of disseminating routes via iBGP, is to use what's called a full mesh of iBGP sessions. Where every router inside an AS, is connected to every other router. Unfortunately, that approach doesn't scale, so many large networks use a technique called route reflection. Route reflection improves scaling, but there are potential problems with route dissemination, if the route reflector hierarchy is not configured correctly. A route reflector, will reflect all of its client routes to all other routers. But any route that it learns from a router that's not a client, it will only re-advertise to its clients. Here's an example of a route reflector hierarchy that results in a path visibility problem. When a route arrives from a neighboring autonomous system, the route reflectors re-advertise routes only to the clients. The clients, on the other hand, do not re-advertise routes to other route reflectors. So, the route that X learns via iBGP would not be re-advertised to the route reflector Y, in this route reflector hierarchy. The upshot of this misconfiguration is that Y and Z actually don't learn a route to the destination, which can turn out to be a real debugging nightmare. We need to come up with a constraint that we can check against the configuration to detect this type of fault, automatically. It turns out, that in this case, the check for correctness of path visibility is simple. All we need to do is check that the set of routers that are not route reflector clients for any other routers, form a full mesh. In other words, they should all be connected to one another. Once this property is satisfied, then path visibility would be satisfied. This condition is easy to check, with static analysis of the routing configuration. Another correctness property is route validity. Which says that every route a router learns, should correspond to a usable path. Possible route validity faults include unintentionally providing transit service between two peering ASs, advertising routes that violate higher level policy, or originating routes for private, or unowned address space. Such as in a route hijack. Possible route visibility faults in dissemination, include route advertisements that can result in forwarding loops, or what are called deflections, where traffic is deflected off the advertised path. One example of something we can check that relates to route validity, is consistent export. The rules of settlement-free peering, dictate that two peers should advertise routes at all of the peering points. And the advertised routes, should have equal AS path length. In other words, the routes that one peer advertises to another, should be equally good. This constraint enables what's called hot potato routing. In other words, the AS should be able to choose the exit over which it sends traffic to its peer. It is relatively straightforward to check for consistent export through static analysis of router configuration. In general, however, verifying the correctness of a network by analyzing routing configuration, is extremely hard. It requires analyzing distributed low-level configuration, and checking correctness constraints based on an inferred model of how the network protocols might be behaving. On the other hand, SDN allows us to treat verification as a distributed program, applying concepts from software engineering, testing and formal verification, to check the correctness of a network. In the coming lessons, we'll look at how these techniques can be used to verify both the control plane and the data plane.
