# An Extensible Automated Failure Localization Framework Using NetKAT, Felix, and SDN Traceroute
## 2 Background
### Formal Description of Networks  
Having an easily configurable controller is key in operating software-defined networks successfully. In order to achieve this goal, the Frenetic project developed their controller platform around a new formal language, NetKAT. It was specified in a way to make network description simple and allow reasoning about the properties of the described network as well [6]. The language differsfrom previous approaches for describing networks in that it can incorporate information on both network topology and forwarding behavior. This is supported on both a very high level as well as lower levels. The Frenetic project developed tools that are able to parse high level topology and policy descriptions and--through a series of steps--compile them into low-level instructions, at the end transforming them directly to OpenFlow flow table entries. In the following, we first introduce the language in more detail, then we shortly present how the compilation from high-level description to low-level instructions works. The NetKAT Language  
The language's concept builds on the assumption that computer networks--under certain conditions--can be modeled with finite state machines and thus can be described by a language using regular expressions. Language rules are based on the Kleene algebra and use KAT (Kleene Algebra with Tests) expressions as building blocks [6]. In NetKAT's view, as detailed in Table 1, packets are considered as records consisting of header fields on which we can execute different operations. These header fields are the usual packet header fields complemented with two additional ones: Switch and port. With predicate operations, we can write primitive actions (like dropping a packet or negating a header field), while policy operations let us modify packets as well as provide an interface for more advanced composition of predicates. For example, the \(+\) operator describes branches in the forwarding and the \(\cdot\) operator describes consecutive network nodes or processing events. The \(=\) testing operator is also defined, which is used for filtering packets matching specified header fields or switch identifiers. The \(\leftarrow\) assignment operator is used for assigning new values to fields. Using this interpretation, the following expressions describe the topology containing a single link shown in Figure 3:  
\[(\mathrm{sw}=1\cdot\mathrm{pt}=2\cdot\mathrm{sw}\gets 2\cdot\mathrm{pt} \gets 1)+(\mathrm{sw}=2\cdot\mathrm{pt}=1\cdot\mathrm{sw}\gets 1 \cdot\mathrm{pt}\gets 2).\]  
Here we have two expressions that describe forwarding on the link. The first one specifies the _Switch 1_ to _Switch 2_ direction, while the second gives the reverse direction. If we imagine the network as an entity that performs transformations on packets, we can easily understand the idea behind the notation. First, with \(\mathrm{sw}=1\cdot\mathrm{pt}=2\), we select packets that arrive to port 2 of Switch 1. Then we describe the transformation that a link applies to these packets: It modifies the \(\mathrm{sw}\) (switch) filed to 2 and \(\mathrm{pt}\) (port) to 1. \begin{table}
\begin{tabular}{l l l} \hline Fields & \(f::=f_{1}|\ldots|f_{k}\) \\ Packets & \(pk::=\{f_{1}=v_{1},\ldots,f_{k}=v_{k}\}\) \\ Predicates & \(a,b::=1,\) & identity \\  & \(0,\) & drop \\  & \(f=n,\) & test \\  & \(a+b,\) & disjunction \\  & \(a\cdot b,\) & conjunction \\  & \(-a,\) & negation \\ Policies & \(p,q::=\) & \(a,\) & filter \\  & \(f\gets n,\) & modification \\  & \(p+q,\) & union \\  & \(p\cdot q,\) & sequential composition \\  & \(p^{*},\) & Kleene star \\  & \(\mathrm{dup},\) & duplication \\ \hline \end{tabular}
\end{table} 
Table 1: NetKAT syntax [6]. Figure 3: A simple network with a single link.