Skip to main content
To refer to this page use:
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.
Publication Date: Jun-2016
Citation: Beckett, Ryan, Michael Greenberg, and David Walker. "Temporal NetKAT." In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (2016): pp. 386-401. doi:10.1145/2908080.2908108
DOI: 10.1145/2908080.2908108
Pages: 386 - 401
Type of Material: Conference Article
Journal/Proceeding Title: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation
Version: Author's manuscript

Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.