So the next thing we will look at is what is called Header Space Analysis. So here the idea is that, once again, it comes back to what I said earlier, that if you take any packet, the payload is uninteresting. The header is the one thing that is interesting. You can say that every bit in the header, if you have an L-bit header, every bit in the header is either going to be a zero or a one, and if I have L-bits in the header, then you can think of a header as basically a point in an L-dimensional hyperspace, because they are L bits, and each of these L-bits can be a zero or a one. So in an L-dimensional hyperspace, it's a point. If you look at any particular switch in this networking fabric, what is the switch doing? Well, it is not doing anything to the payload, all it is doing is it is doing a transformation on the header. So it is transforming the header from the input to the output. So for instance, a header starts out to be this, and it changes to this by the time it comes out of T_3. Not all of the bits of the header are also changing. So if you take a header, the header contains probably a sequence number, a host address, and destination, and many of those things don't change. Maybe the thing that changes is how many hops has this packet already taken and things like that. So the transformation that's happening is very simple. So the packet header, first of all, is appointed the L-dimensional hyperspace, and we're going to model all the network boxes like this, we're going to model them as a transformer on the packet header space. The header space analysis basically defines an algebra for this transformation. Meaning, if you look at what is going on to this packet from source to destination, first of all, this guy does the transformation. So T_1 does a transformation on the input header, and then that is going through another level of transformation by T_2. So T_2 is doing a transformation on that. Then finally, T_3 is doing a transformation on that, and that becomes the output header. This is the is a composable algebra that says that these transformations are composable from source to destination. It is also invertible. What I mean by that is if I have the input header, I can say that the input header is the inverse of this transformations. So inverse of T_3, followed by T_2 inverse, followed by T_1 inverse of the output. So the algebra that you defined is composable and invertible so that you can derive what has happened to the packet from source to destination. The nice thing about this is that this model, the header space analysis model is completely agnostic to what protocol is being used, what is the network topology that is being employed, and it can model all kinds of forwarding functionalities regardless of what specific protocol is being used, and how it is implemented. So that's a nice thing about this header space analysis. This is just the theory behind this. Now, to put it to work, they built a tool, and that's what we will look at in a minute. So in terms of using the model, all the traffic flows can be expressed as a series of transmission using the algebra. Because the algebra is powerful, and you can set it in motion, and we can ask questions like, can two hosts communicate with each other? Are there forwarding loops? Are there network partition? Meaning that if I have a network and some links are broken from here to here, then you cannot get to this partition, and these are the algebra that the header space analysis is giving you as a powerful way of detecting such partitions when they do happen. The tool that they've built on top of header space analysis is called NetPlumber. So basically what this NetPlumber does is it creates a dependency graph of all the forwarding rules, just like what I just now mentioned in the network, and uses it to verify policies. So you have nodes in the graph will be derived from the switches, but in particular, with respect to what are the forwarding functions implemented by a particular switch. So for instance, if this switch can send packets here, then it has an edge to that. Even though, for instance, this guy is connected to all three switches here, but let's say that the forwarding rules in this doesn't have any way of taking packets to this side, then it won't have a directed edge between here and here. So that's how you'll construct the nodes in the graph and directed edges which are next-hop dependency of the forwarding rules. So let's take a concrete example here. Suppose that we have this set of forwarding rules set in this switch that says green packets go this way, red packets go this way, and purple packets go this way. That's the forwarding rule that had been set up here. So we will have the graph formulation of this. It will say that, let's say a give a number. This is S_1, S_2, S_3, and S_4. So we've got a graph in which I have a forwarding rule to S_2, and a forwarding rule to S_5, and similarly, a forwarding rule to S_3. So these are the rules that have been set up, and corresponding to that, you can think of a graph that NetPlumber has, that'll have the nodes in the graph which will be the switches, and the edges are the forwarding rules that are applied from that switch. So given this, you have a way of analyzing different things. So for instance, if things change, so right now, purple packets flow this way, and red packets flow this way, and green packets flow this way, and if things change, and I decided that instead of sending the purple packets this way, I want to change the forwarding rules to something else, then all that I have to do is incrementally update only trees through the dependency subgraph that is affected by the update to the forwarding policy. Again, when it comes to scalability of this analysis, you can reduce the state space over which you have to do this analysis by looking at only the incremental update that you have to apply based on the forwarding rules changes. So that's what gives you both the flexibility of policy expression, and also reducing the complexity of the third space that is involved, and knowing what's going on in the network. You can also have the opportunity to parallelize, you can partition the dependency graph into clusters to minimize the inter-cluster dependency. So that is another thing that you can do to make this more scalable too. So these are the things that are available as tools that you can use for recognizing what may be going on in the network, whether there's anything that is happening that resulting in errant behavior of your network. You can analyze that using these tools.