Temporal NetKAT

Ryan Beckett, Michael Greenberg, David Walker

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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

Publication series

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

Other

Other37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016
CountryUnited States
CitySanta Barbara
Period6/13/166/17/16

All Science Journal Classification (ASJC) codes

  • Software

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

    Beckett, R., Greenberg, M., & Walker, D. (2016). Temporal NetKAT. In C. Krintz, & E. Berger (Eds.), PLDI 2016 - Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (pp. 386-401). (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI); Vol. 13-17-June-2016). Association for Computing Machinery. https://doi.org/10.1145/2908080.2908108