Temporal NetKAT

Ryan Beckett, Michael Greenberg, David Walker

Research output: Contribution to journalArticlepeer-review

Abstract

Over the past 5-10 years, the rise of software-defined networking (SDN) has inspired a wide range of new systems, libraries, hypervisors and languages for programming, monitoring, and debugging network behavior. Oftentimes, these systems are disjoint-one language for programming and another for verification, and yet another for run-time monitoring and debugging. In this paper, we present a new, unified framework, called Temporal NetKAT, capable of facilitating all of these tasks at once. As its name suggests, Temporal NetKAT is the synthesis of two formal theories: past-time (finite trace) linear temporal logic and (network) Kleene Algebra with Tests. Temporal predicates allow programmers to write down concise properties of a packet's path through the network and to make dynamic packet-forwarding, access control or debugging decisions on that basis. In addition to being useful for programming, the combined equational theory of LTL and NetKAT facilitates proofs of path-based correctness properties. Using new, general, proof techniques, we show that the equational semantics is sound with respect to the denotational semantics, and, for a class of programs we call network-wide programs, complete. We have also implemented a compiler for temporal NetKAT, evaluated its performance on a range of benchmarks, and studied the effectiveness of several optimizations.

Original languageEnglish (US)
Pages (from-to)386-401
Number of pages16
JournalACM SIGPLAN Notices
Volume51
Issue number6
DOIs
StatePublished - Jun 2016

All Science Journal Classification (ASJC) codes

  • General Computer Science

Keywords

  • Domain-specific languages
  • Kleene algebra with tests
  • NetKAT
  • Network programming languages
  • Temporal logic

Fingerprint

Dive into the research topics of 'Temporal NetKAT'. Together they form a unique fingerprint.

Cite this