Temporal NetKAT

Ryan Beckett, Michael Greenberg, David Walker

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

15 Scopus citations

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 pathbased 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
Title of host publicationPLDI 2016 - Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation
EditorsChandra Krintz, Emery Berger
Pages386-401
Number of pages16
ISBN (Electronic)9781450342612
DOIs
StatePublished - 2 Jun 2016
Event37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016 - Santa Barbara, United States
Duration: 13 Jun 201617 Jun 2016

Publication series

NameProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
Volume13-17-June-2016

Conference

Conference37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016
Country/TerritoryUnited States
CitySanta Barbara
Period13/06/1617/06/16

Keywords

  • Domain-specific languages
  • Kleene algebra with tests
  • Netkat
  • Network programming languages
  • Software-defined networking
  • Temporal logic

Fingerprint

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

Cite this