KATch: A Fast Symbolic Verifier for NetKAT

TL;DR

This work develops new data structures and algorithms for checking verification queries in NetKAT, a domain-specific language for specifying the behavior of network data planes, and presents KATch, an implementation of these ideas in Scala, featuring an extended set of NetKAT operators that are useful for expressing network-wide specifications.

Abstract

We develop new data structures and algorithms for checking verification queries in NetKAT, a domain-specific language for specifying the behavior of network data planes. Our results extend the techniques obtained in prior work on symbolic automata and provide a framework for building efficient and scalable verification tools. We present KATch, an implementation of these ideas in Scala, featuring an extended set of NetKAT operators that are useful for expressing network-wide specifications, and a verification engine that constructs a bisimulation or generates a counter-example showing that none exists. We evaluate the performance of our implementation on real-world and synthetic benchmarks, verifying properties such as reachability and slice isolation, typically returning a result in well under a second, which is orders of magnitude faster than previous approaches. Our advancements underscore NetKAT's potential as a practical, declarative language for network specification and verification.

Figures (12)

• Figure 1: NetKAT syntax and semantics.
• Figure 2: Bisimulation algorithm à la Hopcroft & Karp Hopcroft1971
• Figure 3: Examples of $\mathsf{SP}$s, where $p \triangleq (a\mathrel{\!=\!}3 \cdot b\mathrel{\!=\!}4 \mathrel{+} b \mathrel{\!\neq\!} 5 \cdot c\mathrel{\!=\!}5)$ and $q \triangleq (b=3 \cdot c\mathrel{\!=\!}4 \mathrel{+} a\mathrel{\!=\!}5 \cdot c \mathrel{\!\neq\!} 5)$.
• Figure 4: Definition of the $\mathsf{SP}$ operations. The inductive case is identical for all operations (indicated by $\mathrel{\mathop{\hat{\pm}}}$), and applies when both $\mathsf{SP}$s test the same field. Expansion inserts a trivial $\mathsf{SP}$ node to reduce the remaining cases to the inductive case. The notation $b(v;d)$ means the child $b(v)$ if $v \in \textsf{dom}(b)$, or the default case $d$ otherwise.
• Figure 5: Examples of SPPs, where $p \triangleq (a \mathrel{\!=\!} 5 + b \mathrel{\!=\!} 2) \cdot (b \mathrel{\!\shortleftarrow\!} 1 + c \mathrel{\!=\!} 5)$, and $q \triangleq (b \mathrel{\!=\!} 1 \mathrel{+} c \mathrel{\!\shortleftarrow\!} 4 \mathrel{+} a \mathrel{\!\shortleftarrow\!} 1 \cdot b \mathrel{\!\shortleftarrow\!} 1)$.

Theorems & Definitions (19)

• definition 1: Reduced and Ordered
• lemma 1
• lemma 2
• corollary 1
• lemma 3
• theorem 1: RO form is unique
• theorem 2
• definition 2: Reduced and Ordered
• lemma 4
• corollary 2