TY - GEN
T1 - Temporal NetKAT
AU - Beckett, Ryan
AU - Greenberg, Michael
AU - Walker, David
N1 - Publisher Copyright: © 2016 ACM.
PY - 2016/6/2
Y1 - 2016/6/2
N2 - 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.
AB - 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.
KW - Domain-specific languages
KW - Kleene algebra with tests
KW - Netkat
KW - Network programming languages
KW - Software-defined networking
KW - Temporal logic
UR - http://www.scopus.com/inward/record.url?scp=84975880710&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84975880710&partnerID=8YFLogxK
U2 - 10.1145/2908080.2908108
DO - 10.1145/2908080.2908108
M3 - Conference contribution
T3 - Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
SP - 386
EP - 401
BT - PLDI 2016 - Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation
A2 - Krintz, Chandra
A2 - Berger, Emery
PB - Association for Computing Machinery
T2 - 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016
Y2 - 13 June 2016 through 17 June 2016
ER -