# An Extensible Automated Failure Localization Framework Using NetKAT, Felix, and SDN Traceroute
## 2 Background
### Host Monitoring with Felix  
In conjunction with the above aspects of the Frenetic controller, a network monitoring tool was also developed [12]. The main idea behind the tool is to put the least strain possible on network equipment during monitoring. It is split into different components. The first one is the _Felix compiler_, which is a decision service that is able to determine the type of traffic in which hosts should be monitored when checking a path in the network. Parallel to this, a _measurement service_ runs on each host of the monitored network and logs incoming and outgoing packets. Lastly, a _controller_ is responsible for connecting the previous two. In the following, we give a summary about the first two, since in our work, the controller was replaced by our framework. Figure 5: Frenetic compilation process. Felix Compiler  
Felix is able to parse network descriptions and, based on a path definition, compute the parameters of the traffic passing through the path at hand. Thus, in order to find out these parameters, we need to supply Felix with network inputs and outputs, policy and topology NetKAT descriptions, as well as a path definition. The first four can be obtained as discussed above, while the last one should be supplied manually. The path definition--or query in Felix terminology--can define links in the network, and its syntax is given by Table 2. A filter expression defines the input and output behavior like end points of a link. Other operators can be used for combining such links into a path. Let us take an example of how Felix works on the network shown in Figure 4. Assume that we would like to check the path _switch 3 \(\rightarrow\) switch 4 \(\rightarrow\) switch 2_. We have already defined the network topology in the previous section; thus, we only need to create an expression that specifies the selected path. Our first guess could be listing the links in the path as \(\text{path}_{\text{naive}}\) does below. However, this way, we specify a path that starts at exactly _switch 3_. Unfortunately, this point cannot be the start of any traffic in the network we specified, since traffic can originate only from network inputs, and _switch 3_ is not one of those. Thus, we have to add a wildcard expression that matches any link preceding the first one, as given by query path:  
\[\text{path}_{\text{naive}}=(\text{sw}=3,\,\text{sw}=4)\cdot( \text{sw}=4,\,\text{sw}=2)\] \[\text{path}=(\text{true, true})^{*}\cdot(\text{sw}=3,\,\text{sw}=4 )\cdot(\text{sw}=4,\,\text{sw}=2)\cdot(\text{true, true})^{*}.\]  
As a response, we receive only one host pair. The reason for this amount is that only the traffic between these two uses the given path. In the result, we find an alpha host that specifies the properties of the starting point and a beta host that gives the destination of the traffic. In the below expression, alpha means that packets sent to _host 2_ should be monitored on the host connected to _port 1_ of _switch 1_. Similarly, beta specifies the receiving side:  
\[\text{alpha} =[\text{dst}\gets 2\cdot\text{pt}\gets 1\cdot\text{sw} \gets 1]\] \[\text{beta} =[\text{dst}\gets 2\cdot\text{pt}\gets 2\cdot\text{sw} \gets 5].\]  
Likewise, if we were to test the link between switches 2 and 5, we would write a slightly different path query. This case would now supply us with more host pairs:  
\[\text{path}=(\text{true, true})^{*}\cdot(\text{sw}=2,\,\text{sw}=5)\cdot( \text{true, true})^{*}\]  
\[\text{alpha} =([\text{dst}\gets 2\cdot\text{port}\gets 4\cdot \text{switch}\gets 2],\,[\text{dst}\gets 2\cdot\text{port}\gets 1 \cdot\text{switch}\gets 1])\] \[\text{betas} =([\text{dst}\gets 2\cdot\text{port}\gets 2\cdot\text{switch} \gets 5],\,[\text{dst}\gets 2\cdot\text{port}\gets 2\cdot\text{switch} \gets 5]).\]  
As we defined the path with a certain direction, we still receive host pairs generating and receiving traffic only in that direction. In order to test both directions, we could reverse the order of links and