NetKAT: Semantic Foundations for Networks

• SDN 41
• programming 8

http://www.cs.cornell.edu/~jnfoster/papers/frenetic-netkat.pdf

equational theory. … design of NetKAT, including primitives for filtering, … We show that NetKAT is an instance of a canonical and well-studied mathematical structure called Kleene algebra with tests (KAT) and prove that its equational theory is sound and complete with respect to its denotational semantics.

Traditional network devices have been called “the last bastion of mainframe computing”[9]¹ … since the 1970s: out of special-purpose devices such as routers, switches, firewalls, load balancers, and middleboxes, each implemented with custom hardware and programmed using proprietary interfaces. this design makes it difficult to extend networks with new functionality and effectively impossible to reason precisely about their behavior.

Network programming languages

… domain-specific languages for SDN [5–7, 23–25, 31, 32]. The goal of thes network programming languages is to raise the level of abstraction of network programs above hardware-oriented APIs such as OpenFlow.