# An Extensible Automated Failure Localization Framework Using NetKAT, Felix, and SDN Traceroute
## 2 Background
### Formal Description of Networks
In that latter case, the network could be split into slices having their own subpolicies that can be combined into a single network-wide policy. Let us see an example now for verifying that UDP traffic from _host 1_ to _host 2_ can traverse the network. Solving the following inclusion would mean that our assumption (UDP traffic can pass through the network) is included in the network behavior (axioms for the deduction are detailed in [6]):  
Figure 4.4  
From the above examples, we can see that describing network topologies is quite an easy feat even on a low level. The process can be done programmatically, and we leverage this feature in the implementation of our framework as well. Policies, in cases of complex networks, can be harder to build, though. Every network should have a high-level policy that describes the grand scheme of network operation, but deriving low-level instructions from this is a tough job. Fortunately, Frenetic is so ambitious that it is able to compile such high-level forwarding descriptions into low-level policies and eventually turn them into OpenFlow flow table entries. We highlight the main considerations of the steps taken by the process in the following. The process applies a three-stage workflow [19] to transform high-level network specifications into low-level instructions, as shown in Figure 4.5 In the first stage, a \(v\) virtual program specifiesthe high-level forwarding behavior of the network on a \(vt\) virtual topology. The virtual topology can be a simplification of the real network, e.g., a big switch that is directly connected to every host in the network. This separation of virtual and physical network descriptions has the benefit that changes in the physical network will have no effect on the specification of high-level forwarding behavior. The \(vc\) virtual compiler then takes \(v\) and \(vt\), together with an \(m\) mapping between the real and virtual networks and distills them into a \(g\) global program. This defines routes between virtual ports using physical paths. A global program can combine expressions specifying processing jobs in switches and defining network topology. It can also contain additional state information that cannot be added on a lower level. After this, the \(gc\) global compiler produces a \(p\) local program from \(g\) that lists the low-level policy rules of the network in the form discussed above. In the last stage of the compilation process, the \(lc\) local compilation step takes the \(p\) network policy and the \(t\) physical topology together with network inputs and outputs and combines them using the formula discussed above: inputs \(\cdot\left(p\cdot t\right)^{*}\) - outputs. In the end, the compilation creates OpenFlow forwarding tables for each switch with the help of forwarding decision diagrams. Since a broad range of networks can be described by the NetKAT language, we believe it is optimal to be used as a method for formally specifying networks for our framework. Using the language axioms, we can deduce forwarding behavior based on specifications written in NetKAT. Our framework thus needs to discover path information from the specification, and while it would be possible to use a proprietary engine for this purpose, we decided to use the one that has been developed within the scope of the Frenetic project. The tool is called Felix, and it is able to generate test cases for paths in a network and monitor forwarding behavior at the hosts. We give more details in the following section about this tool.