PDNet: A Programming Language for Software-Defined Networks with VLAN

Abstract

Software-Defined Networking (SDN) is an emerging networking paradigm, which separates the network’s control logic from the underlying routers and switches, providing the ability to program network, simplifying network management and creating an environment for network evolution. NetKAT is a domain-specific language for specifying and verifying packet-processing functions in software-defined networks (SDNs). This paper proposes a more powerful programming language, PDNet, extending NetKAT to specify the behaviors of SDNs that support virtual local area network (VLAN) tags. We present the operational semantics of PDNet in terms of automata and a syntactic derivatives. When comparing PDNet and NetKAT we show that PDNet is strictly more expressive than NetKAT. As expected, we also show that PDNet is as expressive as NetKAT when describing SDNs without VLAN.

1 Introduction

Traditional network devices, such as switches, routers, firewalls, etc. are built by different vendors out of special purposes. Due to all kinds of custom hardware and interfaces, it is hard to configure traditional networks. Besides, the control plane (that decide how to handle network traffic) and the data plane (that forwards traffic) are bundled inside the networking devices, reducing flexibility and hindering innovation and evolution of the networking infrastructure [1]. The emergence of Software-Defined Networking (SDN) [2], a new network paradigm, has brought a foundational shift on this respect.

It is impossible to reason precisely about legacy network behaviors, which makes it hard to apply formal methods to verify network correctness. SDN offers the Internet community another chance to develop the right kind of architecture and abstractions. This has also led to a great resurgence in interest of applying formal methods to specification, verification, and synthesis of networking protocols and applications [3]. NetKAT [4] is a network programming language, which is used for specifying and verifying the packet-processing behavior of software-defined networks (SDNs). The operational semantic of NetKAT has been presented in [5] in terms of deterministic NetKAT automata. Given a NetKAT expression, a corresponding deterministic NetKAT automaton can be built following the syntactic derivative. The language accepted by a NetKAT automaton is a regular language, which makes it possible to reason about the correctness of a NetKAT program using the equational theory presented in [4].

However, regular expressions are not enough to describe some network behaviors especially when it include the usage of virtual local area network (VLAN). A VLAN is a broadcast domain that is partitioned and isolated in a computer network at the data link layer (OSI layer 2) [6]. It is commonly used in all network virtualization technologies because of its dynamic character. VLAN tags are a useful mechanism for limiting the scope of broadcast traffic, enforcing security and privacy policies, simplifying access control, decentralizing network management, and enabling host mobility [7]. In a SDN, network administrators can configure and manage VLANs more flexibly and efficiently using the OpenFlow protocol [8], the de-facto standard communication protocol between a controller and a switch. The newest edition of the OpenFlow protocol supports adding, modifying and removing VLAN tags. A packet may have one or more VLAN tags stored in a stack so that only the outermost (newest) tag can be modify or delete.

In this paper we extend NetKAT with packets supporting a stack to store VLAN tags. We use three actions in PDNet ($push(v),\,f_0\leftarrow v,$ and pop) to add, modify and remove a tag separately. The main contributions of our work are listed as below:

• Propose a new programming language, PDNet, to describe the behaviors of SDNs based on NetKAT. The ability to describe VLANs makes our language more expressive than NetKAT.

• Study the operational semantics of PDNet, presented in terms of PDNet automata. A PDNet automaton can be built from a PDNet expression following the syntactic derivatives.

• Prove that PDNet is as expressive as NetKAT when restricting the syntax to no VLAN stack manipulating actions.

• Show that PDNet is more expressive than NetKAT.

To help the proofs, we will give a novel definition of nondeterministic NetKAT automata and the corresponding syntactic derivatives.

2 Preliminaries

2.1 SDN and OpenFlow

As shown in Fig. 1, a SDN has three layers. A single-controller OpenFlow-based network has one controller, some switches and some hosts. When a switch receives a packet, it will search its flow table to find a matching rule for the packet. If the matching rule exists, then the switch will forward the packet out through the port specified by the rule. Otherwise, the switch will inform the controller of receiving an unmatched packet, and then the controller will insert a rule into the flow table of the switch to tell the switch how to deal with the packet.

Fig. 1.

SDN structure

Fig. 2.

An example of VLANs

2.2 VLAN

A VLAN allows to break one physical switch into smaller mini-switches, or extend a smaller virtual switch across multiple physical switches. In Fig. 2 we show an example of a network where there are two physical switches and three VLANs (VLAN 10, VLAN 20, and VLAN 30). Notice that VLAN 10 has been extended onto a second switch, which enables Host B and Host C to exist in the same VLAN, despite being connected to different physical switches. Assuming that host C is sending a packet to host B. The packet header C|B|(VLAN)|Type is a standard Layer 2 header. At first, the packet enters VLAN 10 through the access port on switch Y (Y:1), and a tag $\#10$ is added into its header. Then the tagged packet is flooded to all the ports inside the red circle of switch Y except the port that received the packet. Port Y:2 is an access port that connects to switch X, the VLAN tag of every packet that leaves VLAN 10 through Y:2 will be removed. When the packet from host C to host B arrives at port X:2, the tag $\#10$ is added into its header again.

Notice that, in nested VLANs, it is possible that a packet has more than one VLAN tag, and any action on VLAN tags only acts on the outermost (newest) tag. In the OpenFlow protocol, there are three actions that are related to VLAN.

• $Push\_tag\textit{:}$ Push a new VLAN tag onto the packet. A newly pushed tag should always be inserted in the outermost valid location of the VLAN field.

• $Pop\_tag\textit{:}$ Pop the outermost VLAN tag from the packet.

• $Set\_tag\textit{:}$ Set the ID of the outermost VLAN tag.

2.3 Syntax of NetKAT

Forwarding a packet from node to node in a network can be seen as moving from state to state in an automaton. Therefore, it is natural to use regular expression to describe the forwarding behavior of a network. For example, the concatenation of a series of forwarding behaviors specifies a path. Moreover, Kleene algebra (KA) [9], a sound and complete equational theory for regular expressions, can be used to reason about properties of networks.

NetKAT is an instance of Kleene algebra with tests (KAT) [10]. KAT is a two-sorted algebra $(K,B,+,\cdot ,*,\bar{},0,1)$, where $B\subseteq K$:

A Kleene algebra consists of three operators and two constants: choice ($+$), sequential composition operator ($\cdot$), iteration ($*$), fail (0) and skip (1). ($\cdot$) is usually elided in expressions. B is the set of tests. When applied to tests, ($+$) and ($\cdot$) act as disjunction and conjunction respectively. ( $^{\bar{}}$ ) is the Boolean negation operator defined only on B. We let p, q, r, s, t range over arbitrary elements of K and a, b, c, d over tests in.

Table 1. Syntax and operational semantics of NetKAT

The syntax of NetKAT is shown in Table 1. A packet pk is a packet record that composes of k fields, including the header values and the location information. A sequence of packet forms a history, which records the states of a packet as it travels in the network. A policy specifies the behaviors of a switch. A predicate models the filtering process of a switch. Predicates may have true (1), false (0), test ($f\,=\,v$), conjunctions, disjunction, and negation ($\lnot a$). An assignment ($f\,\leftarrow \, v$) assigns value v to the field f. A test ($f\,=\,v$) checks whether the field f is equal to v. (dup) records the current state of a packet into the history. $\alpha$ is a complete test, and $\pi$ is a complete assignment. $f_1,\cdots ,f_k$ are in some arbitrary but fixed order. $\alpha _\pi$ is the complete test corresponding to the complete assignment $\pi$, and $\pi _\alpha$ is the complete assignment corresponding to the complete test $\alpha$. The operator precedence is: $(*)> ({\cdot }) > ({+})$.

Example 1

As shown in Fig. 3, Host $H_0$ sends packets to host $H_1$ via two switches: $S_0$ and $S_1$. A packet is composed of source address (src), destination address and two fields: switch (sw) and port (pt). The policy for switch $S_0$ is encoded as:

$$\begin{aligned}&p_0\,\triangleq \,(sw=S_0\,\cdot \,pt=P_1\,\cdot \,dst=H_1\,\cdot \,pt\leftarrow P_2) \end{aligned}$$

It specifies that for a packet whose current location is port $P_1$ of switch $S_0$, and its destination address is $H_1$, forward the packet out through port $P_2$.

Fig. 3.

Example network for NetKAT

2.4 Operational Semantics of NetKAT

The definition of deterministic NetKAT automata is illustrated in Table 1.

• S is a finite set of states;

• $\delta$ is a continuation map, which specifies transitions from one state to another state;

• $\varepsilon$ is an observation map, which records information of each state;

• $s_0$ is a distinguished start state.

Every NetKAT expression (policy) p can be interpreted as a subset of $At\cdot \varPi \cdot (dup\cdot \varPi )^*$. Here At is the set of complete tests, and $\varPi$ is the set of complete assignments. The language G(p) of a NetKAT expression p is the set of strings accepted by the finite NetKAT automaton associated with p [5].

Observing the string $\alpha \, \pi _1\, dup\,\pi _2$, we can think of it as $\alpha \,\beta _{\pi _1}\,\beta _{\pi _2}$, where $\alpha$ is the precondition and $\beta _{\pi _1}$ denotes the postcondition after doing the assignment $\pi _1$. The placeholder dup is used to record the postcondition after the first assignment. We can write postconditions explicitly and omit assignments as well as duplications, and as a result, the language accepted by a deterministic NetKAT automaton is just a subset of $At\times At\times At^*$.

Fig. 4.

An example of deterministic NetKAT automata

Example 2

Figure 4 shows a simple deterministic NetKAT automaton and the strings it accepts. There are four states (X, Y, Z, 0). The three vertical arrows without subsequent states represent observation map, and the other arrows stand for continuation map. Assuming the packet consists of two fields, and each field has two possible values, then there are four possible complete tests ($\alpha _1, \alpha _2, \alpha _3, \alpha _4$).

• $Accept_d(X,\alpha _1\alpha _1)=\varepsilon (X,\alpha _1,\alpha _1)=1$, and thus the string $\alpha _1\alpha _1$ is accepted.

• $Accept_d(X,\alpha _1\alpha _2\alpha _1)=Accept_d(\delta (X,\alpha _1,\alpha _2),\alpha _2\alpha _1) =Accept_d(Y,\alpha _2\alpha _1)=\varepsilon (Y,\alpha _2,\alpha _1)=1$, and hence the string $\alpha _1\alpha _2\alpha _1$ is accepted.

3 Nondeterministic NetKAT Automata

In order to prove the relation between NetKAT and PDNet in Sect. 5, next we propose a novel definition of nondeterministic NetKAT automata as well as a corresponding syntactic derivatives. An example of nondeterministic NetKAT automata presented in this section will help understand the semantics of PDNet.

3.1 Automata Definition

As shown in Table 2, a nondeterministic NetKAT automaton ($M_n$) is a 4-tuple ($T,\,\varDelta ,\,E,\,t_0$) where

• T is a finite set of states;

• $\varDelta$ is a continuation map;

• E is a observation map;

• $t_0$ is a distinguished start state.

Table 2. Nondeterministic NetKAT automata

3.2 Syntactic Derivatives

In the bottom of Table 2, we define the non deterministic automata generated by the syntactic derivatives of a NetKAT expression. Exp is a superset of reduced NetKAT expressions that include arbitrary tests b. Every NetKAT expression is provable equivalent to a reduced NetKAT expression, where each assignment is a complete assignment and each test is a complete test.

Example 3

An example is shown below to explain how to build a corresponding nondeterministic automaton from a reduced NetKAT expression. Let the packet have two fields ($f_1$, $f_2$), and each field has two possible values ({0, 1}). Thus the set of possible complete tests is $At=\{f_1=0\cdot f_2=0,\,f_1=1\cdot f_2=0,\,f_1=0\cdot f_2=1,\,f_1=1\cdot f_2=1\}$. Let the start expression be $\alpha _1\,\pi _1\,dup\,\pi _2$, where the complete test $\alpha _1$ is $f_1=1\cdot f_2=0$, the complete assignment $\pi _1$ denotes $f_1\leftarrow 0\cdot f_2\leftarrow 0$, and $\pi _2$ is $f_1\leftarrow 0\cdot f_2\leftarrow 1$. Note that $\alpha _\pi$ represents the complete test that is corresponding to $\pi$. When we use $\alpha$ without any subscript, it stands for any complete test that belongs to At.

The first step is to compute all the states. The computing process is given as below. The start expression $\alpha _1\,\pi _1\,dup\,\pi _2$ is the initial state, and its subsequent state is the expression $\alpha _{\pi _1}\pi _2$.

The second step is to check whether a state can accept the string that is associated with the state. $E_n(dup,\alpha ,\beta )=0$, and therefore the computation result for any string that combines with dup using the composition operator is 0. Thus, $E_n(\alpha _1\pi _1dup\pi _2,\alpha ,\beta )=0$, and it means that the start state does not accept any string. The computation for the second state is as follows:

$$\begin{aligned} E_n(\alpha _{\pi _1}\pi _2,\alpha ,\beta )=\sum \limits _{\eta }(E_n(\alpha _{\pi _1},\alpha ,\eta )\cdot E_n(\pi _2,\eta ,\beta ))=1\,\,\,IFF\,\,\,\beta =\alpha _{\pi _2} \end{aligned}$$

Finally, according to the computations above, we illustrate the nondeterministic automata for the expression $\alpha _1\,\pi _1\,dup\,\pi _2$ in Fig. 5. We only draw those arrows that lead to accepted strings. The two complete tests on the transition arrow can be thought of the precondition and the postcondition after the assignment $\pi _1$. The postcondition of the first state should be passed to the subsequent state, and that is, $\alpha _{\pi _1}$ is passed to the second state as its precondition.

Fig. 5.

The nondeterministic NetKAT automaton for $\alpha _1\,\pi _1\,dup\,\pi _2$

4 PDNet

4.1 PDNet Syntax

When the network to be programmed is simple, regular expressions are able to specify VLAN fields as long as the programmer remembers the indexes and orders of all the operations on VLAN tags. However, when the network topology is more complex, or there are some changes that need be made (switch functionalities or network structures that involve operations of VLAN tags) in the network, it is tedious to modify all the related policies, since the index of the field that denotes the outermost VLAN tag always needs to be counted carefully.

Instead of using regular expressions, we use a more intuitive and flexible structure to model VLAN tags, and that is stack. As shown in the top of Table 2, we add a field named $f_0$ to store VLAN tags for each packet. Fields $f_1$ to $f_k$ are mapping to integers, while field $f_0$ is mapping to a stack. When a packet traverses VLANs, it at least has one VLAN tag, and therefore, the stack has at least one element. $f_0=v$ denotes checking the top (outermost) tag of the stack, and $f_0\leftarrow v$ stands for assigning v to the top tag. We also have push(v) and pop that are corresponding to adding and removing of a VLAN tag respectively. Note that a complete test or a complete assignment excludes the VLAN field.

Table 3. Syntax and semantics of PDNet

4.2 Operational Semantics of PDNet

Just like NetKAT expressions, each PDNet expression is equivalent to a reduced PDNet expression in which all assignments are complete assignments, and all tests are complete tests. Because there is a stack in each packet, the intuitive thought of developing the operational semantics of PDNet is to use pushdown automata. To take a step further, in order to design model checking algorithms for PDNet, we adopt pushdown system [11] to present the operational semantics. Formally, a pushdown system $\mathcal {P}=(R,\varGamma ,\varPhi ,c_0)$ is a transition system with 4-tuple where:

• R is a finite set of states (control locations);

• $\varGamma$ is a finite stack alphabet;

• $\varPhi$ is a finite subset of $(R\times \varGamma )\times (R\times \varGamma ^*)$, if $((r,\gamma ),(r',\omega ))\,$in $\varPhi$, we can also write it as ${<}r,\gamma {>}\hookrightarrow {<}r',\xi {>}$, where $\xi \in \varGamma ^*$.

• $c_0$ is the initial configuration with the form of ${<}r,\xi {>}$, where $r\in R$ and $\xi \in \varGamma ^*$.

As shown in the middle of Table 3, a PDNet automaton is a nondeterministic pushdown system $M_p$. R is the set of non-terminated states, while $\{*\}$ denotes the termination state. Besides the stack in the input data, we also need to consider the precondition and postcondition of an expression. Therefore a configuration is composed of three elements: state, precondition (or postcondition), and stack symbols, which is slightly different from the standard pushdown system. $\gamma \xi$ denotes the whole stack, and $\gamma$ stands for the top element of the stack. In a PDNet program, there are four actions that involve actions on stack:

• $f_0=v\textit{:}$ the stack is unchanged, and $\omega \in \varGamma$;

• $f_0\leftarrow v\textit{:}$ the top element of the stack is modified, and $\omega \in \varGamma$;

• $push(v)\textit{:}$ a new element is added onto the top of the stack, and $\omega \in \varGamma \times \varGamma$;

• $pop\textit{:}$ the top element of the stack is removed, and $\omega \in \{\epsilon \}$.

Fig. 6.

An example of PDNet automata

Example 4

Figure 6 presents a simple PDNet automaton with three states. The set of possible complete tests is $\{\alpha ,\beta \}$, and $\varGamma =\{1,2\}$. The two transitions from $r_0$ to $r_0$ denote push(1) and push(2) respectively. The transitions from $r_0$ to $r_1$ stand for pop. The strings accepted by the automaton have the form of $\alpha ^n\beta ^n$.

4.3 Syntactic Derivatives

As shown in Table 3, we also give a syntactic derivative for PDNet, which is an instance of PDNet automata. The syntactic derivative is defined as:

$$\begin{aligned}&\varPhi :\,Exp_p\times At\times \varGamma \longrightarrow \mathcal {P}((Exp_p\cup \{*\})\times At\times (\{\epsilon \}\cup \varGamma \cup \varGamma \times \varGamma ))\\&\text {Where}\,\, Exp_p\,\text {is the set of all the strings with the syntax:}\\&e\,{:}{:}{=}\,b\,|\,\pi \,|\,dup\,|\,f_0\leftarrow v\,|\,push(v)\,|\,pop\,|\,e+e\,|\,e\cdot e\,|\,e^*\end{aligned}$$

b is an arbitrary test that is defined in the top of Table 1, while $\pi$ is a complete assignment.

Since Exp and $Exp_p$ are similar, most of the derivation rules are similar to the rules of the syntactic derivative of nondeterministic NetKAT automata. To make the derivation rules simpler, we combine $D_n$ and $E_n$ together to get $\varPhi$. Besides, we delete all the branches that lead to 0. The conversion formula from the syntactic derivative of nondeterministic NetKAT automata to the syntactic derivative of PDNet automata is:

$$\begin{aligned} \varPhi (e,\alpha ,\gamma )=\{(e_1,\beta ,\gamma )|(e_1,\beta )\in D_n(e,\alpha )\}\cup \{(*,\beta ,\gamma )|E_n(e,\alpha ,\beta )=1\} \end{aligned}$$

Where e does not contain any element of $\{push(v),f_0\leftarrow v ,pop,f_0=v \}$.

5 Comparing NetKAT and PDNet

After introducing the syntax and operational semantics of PDNet, we compare NetKAT and PDNet in this section, and it concerns two parts. One is that PDNet can describe some network behaviors that NetKAT cannot, and another one is that PDNet without actions on VLAN tags can specify the same network behaviors as NetKAT.

Theorem 1 (Expressiveness)

There are languages accepted by PDNet automata that cannot be accepted by any NetKAT automata.

Proof sketch

As mentioned before, the strings accepted by PDNet automata may have the form of $\alpha ^n\beta ^n$. For example, the PDNet expression $e\triangleq f_0=1\cdot f_1=0\cdot push(2)^*\cdot f_1=1 \cdot pop^*\cdot f_0=1$ denotes the behavior of letting a packet enter $k(k\ge 0)$ nested VLANs and then leave the k VLANs in the reverse order. The stack alphabet is $\{1,2\}$ and the complete tests are $\{f_1 = 0,\,f_1= 1\}$. The corresponding PDNet automaton is shown in Fig. 6, where $r_0$ corresponds to p, while $r_1$ corresponds to the subexpression $pop^*; f_0=1$. In fact the PDNet automaton for the expression e, although finite, generates an infinite number of configurations, and they are all needed to define the language accepted.

However, it can be proved that a NetKAT automaton cannot recognize this language using standard language theoretical techniques such as distinguishability classes or the pumping lemma [12].   $\square$

Then, we prove the second part: PDNet is as expressive as NetKAT when specifying networks without VLANs. The proof consists of three steps:

• 1. Deterministic NetKAT automata and nondeterministic NetKAT automata are language equivalent.

• 2. The syntactic derivative of deterministic NetKAT automata and the syntactic derivative of nondeterministic NetKAT automata are language equivalent.

• 3. The syntactic derivative of nondeterministic NetKAT and the syntactic derivative of PDNet automata are isomorphic for all PDNet expressions that do not contain push(v), $f_0\leftarrow v$, pop, or $f_0=v$.

Lemma 1

(step 1). Given a nondeterministic NetKAT automaton $(T,\varDelta ,E,t_0)$, we define a deterministic NetKAT automaton $(\mathcal {P}(T),\delta ,\varepsilon , s_0)$:

• $\delta (X,\alpha ,\beta )=\{(t\in T|\exists x\in X\cdot (t,\beta )\in \varDelta (x,\alpha )\}$

• $\varepsilon (X,\alpha ,\beta )=1\iff \exists x\in X\cdot E(x,\alpha ,\beta )=1$

• $s_0=\{t_0\}$, $\mathsf {where}$ $X\in \mathcal {P}(T).$

$\mathsf {Then}$ $\forall \, X \in \mathcal {P}(T)$, $Accept_d(X,\alpha \beta \mathsf {w})=1 \iff \exists x\in X\cdot Accept_n(x,\alpha \beta \textsf {w})=1.$

Proof

$\mathbf{w}={\varvec{\Lambda }:}$

• $Accept_d(X,\alpha \beta )=\varepsilon (X,\alpha \beta )=1\iff$

• $\exists x\in X\cdot E(x,\alpha ,\beta )=Accept_n(x,\alpha \beta )=1$

• $\mathbf{w}=\sigma \cdot \mathbf{w}'$, where $\sigma \in At,\,\mathsf {w'}\in At^*$

• $Accept_d(X,\alpha \beta \sigma \mathsf {w'})=Accept_d(\delta (X,\alpha \beta ),\beta \sigma \mathsf {w'})=1\iff$

• $\exists t\in \delta (X,\alpha \beta )\cdot Accept_n(t,\beta \sigma \mathsf {w'})=1\iff$

• $\exists x\in X\cdot \exists (t,\beta )\in \varDelta (x,\alpha )\cdot Accept_n(t,\beta \sigma \mathsf {w'})=1\iff$

• $\exists x\in X\cdot Accept_n(x,\alpha \beta \sigma \mathsf {w'})=1$    $\square$

Lemma 2

(step 1). Given a deterministic NetKAT automaton $(S,\delta ,\varepsilon ,s_0)$, we define a nondeterministic NetKAT automaton $(S,\varDelta ,E, s_0)$:

• $\varDelta (s,\alpha )=\{(s',\beta )|\delta (x,\alpha ,\beta )=s'\}$, $\mathsf {where}\,s\in S$

• $E(s,\alpha ,\beta )=1\,\,IFF\,\,\varepsilon (s,\alpha ,\beta )=1$, $\mathsf {where}\,s\in S$

• $\mathsf {Then}$ $\forall \, s\in S$, $Accept_n(s,\alpha \beta \mathsf {w})=1\iff Accept_d(s,\alpha \beta \mathsf {w})=1$

Proof

$\mathbf{w}={\varvec{\Lambda :}}$

$Accept_n(s,\alpha \beta )=E(s,\alpha ,\beta )=1\iff \varepsilon (s,\alpha ,\beta )=Accept_d(s,\alpha \beta )=1$

$\mathbf{w}=\sigma \cdot \mathbf{w}'$, where $\sigma \in At,\,\mathsf {w'}\in At^*$

$Accept_n(s,\alpha \beta \sigma \mathsf {w'})=1\iff$

$\exists (t,\beta )\in \varDelta (s,\alpha )\cdot Accept_n(t,\beta \sigma \mathsf {w'})=1\iff$

$\exists (t,\beta )\in \{(s',\eta )|\delta (s,\alpha ,\eta )=s'\}\cdot Accept_n(t,\beta \sigma u)=1\iff$

$\exists t=\delta (s,\alpha ,\beta )\centerdot Accept_n(t,\beta \sigma u)=1\iff$

$\exists t=\delta (s,\alpha ,\beta )\centerdot Accept_d(t,\beta \sigma u)=1\iff$    (hypothesis)

$Accept_d(\delta (s,\alpha ,\beta ),\beta \sigma u)=Accept_d(s,\alpha \beta \sigma u)=1$    $\square$

Similar to the syntactic derivative of nondeterministic NetKAT automata shown in Table 2, the syntactic derivative of deterministic NetKAT automata is composed of a continuous map $D_d$ and a observation map $E_d$.

Lemma 3

(step 2). The automaton $(Exp,D_d,E_d,e_0)$ and the automaton $(Exp,D_n,E_n,e_0)$ are language equivalent.

Proof

By induction of the length of the string.

$\mathbf{w}={\varvec{\Lambda }}$:

• $\varvec{ e=b:}$

  $Accept_d(b,\alpha \beta )=E_d(b,\alpha ,\beta )=[\alpha =\beta \le b]=E_n(b,\alpha ,\beta )=Accetp_n(b,\alpha \beta )$

• $\varvec{e=\pi :}$

• $Accept_d(\pi ,\alpha \beta )=E_d(b,\alpha ,\beta )=[\pi =\pi _{\beta }]=E_n(\pi ,\alpha ,\beta )=Accetp_n(\pi ,\alpha \beta )$

• $\varvec{e=dup,\,e_1+e_1,\,e_1e_2,\,or\,e_1^*:}$ $\cdots$

When $e=dup,\,e_1+e_1,\,e_1e_2,\,or\,e_1^*$, the proofs are similar, and we do not list them here.

$\mathbf{w}=\sigma \cdot \mathsf {w'}$, $\mathsf {where}$ $\sigma \in At,\,\mathsf {w'}\in At^*$:

• $\varvec{e=b:}$

  $Accept_d(b,\alpha \sigma u)=Accept_d(D_d(b,\alpha ,\beta ),\beta \sigma u)=Accept_d(0,\beta \sigma u)=0$

  $Accept_{n}(b,\alpha \sigma u)=1\iff \exists (e',\beta )\in D_n(b,\alpha )\centerdot Accept_{n}(e',\beta \sigma u)$

  $\mathsf {Since}$ $D_n(b,\alpha )=\{\}$, $Accept_n(b,\alpha \sigma u)=0$

• $\varvec{e=\pi :}$

  $Accept_d(\pi ,\,\alpha \beta \sigma \mathsf {w'})=Accept_d(D_d(\pi ,\alpha \beta ),\beta \sigma \mathsf {w'})=Accept_d(0,\beta \sigma \mathsf {w'})=0$

  $Accept_n(\pi ,\,\alpha \beta \sigma \mathsf {w'})=1\iff \exists (e',\beta )\in D_n(\pi ,\alpha )\cdot Accept_n(e',\beta \sigma \mathsf {w'})=1$

  $\mathsf {Since}$ $D_n(\pi ,\alpha )=\{\}$, $Accept_n(\pi ,\,\alpha \beta \sigma \mathsf {w'})=0=Accept_d(\pi ,\,\alpha \beta \sigma \mathsf {w'})$

• $\varvec{e=dup,\,e_1+e_1,\,e_1e_2,\,or\,e_1^*:}$ $\cdots$

The same like before, we omit the proofs for the situations where $e=dup,\,e_1+e_1,\,e_1e_2,\;or\;e_1^*$.    $\square$

Lemma 4

(step 3). Given a PDNet automaton $(Exp, \varGamma ,\varPhi ,e)$ and a nondeterministic NetKAT automaton $(Exp,D_n,E_n,e)$, we define:

• $\varphi (D_n,E_n)(e,\alpha )=\{(e',\beta )|(e',\beta )\in D_n(e,\alpha )\wedge e\ne 0\}\cup \{(*,\beta )|E_n(e,\alpha ,\beta )=1\}$

• $\psi _{D_n}(\varPhi )(e,\alpha )=\{(e',\beta )|(e',\beta )\in \varPhi (e,\alpha )\}$

• $\psi _{E_n}(\varPhi )(e,\alpha ,\beta )=1\iff (*,\beta )\in \varPhi (e,\alpha ).$

Then $\varphi$ is an isomorphism for all the PDNet expressions (e) that do not contain push(v), $f_0\leftarrow v$, pop, or $f_0=v$.

Proof

$$\begin{aligned} \varphi (\psi _{D_n}(\varPhi ),\psi _{E_n}(\varPhi ))(e,\alpha )&=\{(e',\beta )|(e',\beta )\in \psi _{D_n}(\varPhi )(e,\alpha )\wedge e\ne 0\}\\&\quad \cup \,\{(*,\beta )|E_n(e,\alpha ,\beta )=1\}\\&=\{(e',\beta )|(e',\beta )\in \varPhi (e,\alpha )\wedge e\ne 0\}\\&\quad \cup \,\{(*,\beta )|(*,\beta )\in \varPhi (e,\alpha )\}\\&=\varPhi (e,\alpha ),\,\, \mathsf {where} \,\,e\ne 0 \end{aligned}$$

$$\begin{aligned} \psi _{D_n}(\varphi (D_n,E_n))(e,\alpha )&=\{(e',\beta )|(e',\beta )\in \varphi (D_n,E_n)(e,\alpha )\} \\&=\{(e',\beta )|(e',\beta )\in \{(e'',\eta )|(e'',\eta )\in D_n(e,\alpha )\wedge e\ne 0\}\\&\quad \cup \,\{(*,\eta )|E_n(e,\alpha ,\beta )=1\}\}\\&=\{(e'',\eta )|(e'',\eta )\in D_n(e,\alpha )\wedge e\ne 0\}\\&=D_n(e,\alpha ),\,\, \mathsf {where} \,\,e\ne 0 \end{aligned}$$

$$\begin{aligned} \psi _{E_n}(\varphi (D_n,E_n))(e,\alpha ,\beta )=1&\iff (*,\beta )\in \varphi (D_n,E_n)(e,\alpha )\\&\iff \,\,(*,\beta )\in \{(e',\eta )|(e',\eta )\in D_n(e,\alpha )\wedge e\ne 0\}\\&\qquad \qquad \qquad \cup \,\{(*,\eta )|E_n(e,\alpha ,\beta )=1\}\\&\iff \,\,E_n(e,\alpha ,\beta )=1 \end{aligned}$$

$\square$

From Lemmas 1–4, we can conclude Theorem 2.

Theorem 2 (Compatibility)

Automata of NetKAT and PDNet without push(v), $f_0\leftarrow v$, pop, or $f_0=v$ recognize the same class of languages.

6 Conclusion and Future Work

This paper develops a new programming language (PDNet) based on NetKAT to specify the behaviors of software-defined networks. The novel aspect of the language proposed is that PDNet is able to describe the behaviors of adding, removing and modifying VLAN tags. We use a stack in each packet to store VLAN tags and three new actions to handle them. We also give an operational semantics of PDNet based on pushdown system. Each PDNet expression can be transformed into a corresponding PDNet automaton following the rules of the syntactic derivatives.

PDNet automata are not a standard pushdown automata, as the stack is in the input data and not part of the automaton itself. This explains why there is no full recursion in PDNet expressions, but only tail recursion via Kleene star.

The deterministic NetKAT automata have been proposed in [5]. We give here a novel definition of nondeterministic NetKAT automata as well as the syntactic derivative. Finally, we compare PDNet and NetKAT. First, it is possible to construct expressions like $p^nq^n$ in PDNet, which makes the language of a PDNet automaton a context-free language. However, a NetKAT automaton cannot recognize such language. Therefore, PDNet is more expressive than NetKAT. Second, it is proved that PDNet without push(v), pop, $f_0\leftarrow v$ or $f_0=v$ is as expressive as NetKAT.

Other work on NetKAT are mainly concern with probabilistic extension, fast compiler or coalgebraic decision procedure [5, 13, 14]. We do not expect problems with a probabilistic or weighted extension of PDNet, because these already have been well studied in the context of pushdown systems [15, 16]. In the future, we will develop a modeling checking algorithm for PDNet, and then we may check some interesting properties in software-defined networks with VLANs.