# An Extensible Automated Failure Localization Framework Using NetKAT, Felix, and SDN Traceroute
## 2 Background
### Formal Description of Networks
For a bit more complex network, let us take a look at the one shown in Figure 4. Based on the above example, the topology can be given with the following expression:  
\[t_{\text{net}}=(\text{sw}=1\cdot\text{pt}=2\cdot\text{sw}\gets 3 \cdot\text{pt}\gets 1)+(\text{sw}=1\cdot\text{pt}=3\cdot\text{sw}\gets 4 \cdot\text{pt}\gets 3)+\] \[(\text{sw}=2\cdot\text{pt}=1\cdot\text{sw}\gets 3\cdot\text{ pt}\gets 3)+(\text{sw}=2\cdot\text{pt}=2\cdot\text{sw}\gets 5 \cdot\text{pt}\gets 1)+\] \[(\text{sw}=2\cdot\text{pt}=3\cdot\text{sw}\gets 4\cdot\text{ pt}\gets 2)+(\text{sw}=3\cdot\text{pt}=1\cdot\text{sw}\gets 1 \cdot\text{pt}\gets 2)+\] \[(\text{sw}=3\cdot\text{pt}=2\cdot\text{sw}\gets 4\cdot\text{ pt}\gets 1)+(\text{sw}=3\cdot\text{pt}=3\cdot\text{sw}\gets 2 \cdot\text{pt}\gets 1)+\] \[(\text{sw}=4\cdot\text{pt}=1\cdot\text{sw}\gets 3\cdot\text{ pt}\gets 2)+(\text{sw}=4\cdot\text{pt}=2\cdot\text{sw}\gets 2 \cdot\text{pt}\gets 3)+\] \[(\text{sw}=4\cdot\text{pt}=3\cdot\text{sw}\gets 1\cdot\text{ pt}\gets 3)+(\text{sw}=5\cdot\text{pt}=1\cdot\text{sw}\gets 2 \cdot\text{pt}\gets 2).\]  
The equation does no extraordinary feat, it simply lists each link in the network the same way as in the example before. Network hosts can be defined as well by listing their connection points to switches. If we do so, \(t\), the complete network topology, can be given by taking the conjunction of the expressions defining the hosts and the \(t_{\text{net}}\) network:  
\[\text{hosts}=(\text{sw}=1\cdot\text{pt}=1)+(\text{sw}=5\cdot\text{pt}=2)+( \text{sw}=2\cdot\text{pt}=4)\]  
Figure 3:0  
Thus, we start traffic from a host, then traffic traverses the network, and at the end, it reaches another host. Here, hosts are identified by the position they occupy in the list, e.g., _host 1_ is connected to _switch 1 port 1_. We can incorporate layer 2 and layer 3 addresses as well, in order to complement the expression. In this case, we have to distinguish between the directions that specify incoming and outgoing traffic. Thus, the list of hosts would comprise the disjunction of the two subexpressions, while \(t\) describes cases where traffic originates from inputs and terminates at outputs:  
Figure 3:1 Figure 3:2 Figure 3:3  
Figure 3:4 Sample network for demonstrating NetKAT description. Figure 3:5 Figure 3:6 Figure 3:7 Figure 3:8  
A simple forwarding policy for the network can be defined with a short NetKAT expression giving us a low-level network policy. In the below equation, the first two parenthesized expressions define the routes packets that should be taken towards _host 1_ and _host 2_, respectively. In our sample case, every switch should forward packets destined for _host 1_ on _port 1_ and they should send out packets targeting _host 2_ on _port 2_. In the case of _host 3_--defined by the rest of the expression--we can use a different method where we define forwarding ports for every switch individually, e.g., _switch 1_ should send packets for _host 3_ on _port 1_ (see the third parenthesized expression):  
Figure 3:9 Figure 4.0 Figure 4.1  
We can complement these rules on a high level, for example, with a rule that restricts operation only for UDP traffic. Thus, rule \(p_{\text{UDP}}\) modifies rule \(p\), which deals with traffic in general, in a way that it is executed only when the type of the traffic is UDP. Using this, network operation can now be written as taking the sequential composition of a series made from the policy and the network topology with the predicate for inputs being at the beginning and outputs at the end. Or, by simplifying it with the Kleene star operator, which repeats the preceding expression zero or more times:  
Figure 4.2  
Figure 4.3  
At this point, we can use NatKAT's ability to reason about network properties. Such properties can be whether hosts are able to reach each other or if they are separated in certain ways. Waypointing--e.g., untrusted traffic traversing an intrusion prevention system--can also be tested as well as traffic slicing.