Thu 16 Jun 2016 14:00 - 14:30 at Grand Ballroom San Rafael - Software-Defined Networking Chair(s): Todd Millstein

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.

Thu 16 Jun

Displayed time zone: Tijuana, Baja California change

13:30 - 15:00
Software-Defined NetworkingResearch Papers at Grand Ballroom San Rafael
Chair(s): Todd Millstein University of California, Los Angeles
13:30
30m
Talk
Event-driven Network Programming
Research Papers
Jedidiah McClurg University of Colorado Boulder, Hossein Hojjat Cornell University, Nate Foster Cornell University, Pavol Cerny University of Colorado Boulder
Pre-print Media Attached
14:00
30m
Talk
Temporal NetKAT
Research Papers
Ryan Beckett Princeton University, Michael Greenberg Pomona College, David Walker Princeton University
Media Attached
14:30
30m
Talk
SDNRacer: Concurrency Analysis for Software-Defined Networks
Research Papers
Ahmed Elhassany ETH Zürich, Jeremie Miserez ETH Zürich, Pavol Bielik ETH Zurich, Switzerland, Laurent Vanbever ETH Zürich, Martin Vechev ETH Zurich
Media Attached