TY - JOUR
T1 - Temporal NetKAT
AU - Beckett, Ryan
AU - Greenberg, Michael
AU - Walker, David
N1 - Publisher Copyright:
© 2016 ACM.
PY - 2016/6
Y1 - 2016/6
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 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.
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 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.
KW - Domain-specific languages
KW - Kleene algebra with tests
KW - NetKAT
KW - Network programming languages
KW - Temporal logic
UR - http://www.scopus.com/inward/record.url?scp=85119297939&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85119297939&partnerID=8YFLogxK
U2 - 10.1145/2908080.2908108
DO - 10.1145/2908080.2908108
M3 - Article
AN - SCOPUS:85119297939
SN - 1523-2867
VL - 51
SP - 386
EP - 401
JO - ACM SIGPLAN Notices
JF - ACM SIGPLAN Notices
IS - 6
ER -