[talks] Cole Schlesinger will present his Pre-FPO Tuesday, December 9 in CS 402 at 10am (Title: Abstractions for Software-defined Networks)
ngotsis at CS.Princeton.EDU
Tue Dec 2 09:42:19 EST 2014
Cole Schlesinger will present his Pre-FPO Tuesday, December 9, 2014 in CS 402 at 10am.
The member of his committee are:
Dave Walker (advisor), Aarti Gupta and Arjun Guha (readers), Nick Feamster and Jen Rexford (non-readers).
Everyone is invited to attend his talk. The talk title and abstract follow below:
Abstractions for Software-defined Networks
In a Software-Defined Network (SDN), a central, computationally powerful
controller manages a set of distributed, computationally simple switches. The
controller computes a policy describing how each switch should route packets
and populates packet-processing tables on each switch with rules to enact the
routing policy. As network conditions change, the controller continues to add
and remove rules from switches to adjust the policy as needed.
My research focuses on defining new, high-level languages and abstractions for
expressing network policy; defining technical mechanisms for reasoning formally
about those abstractions; and defining algorithms for compiling high-level
abstractions into available low-level mechanisms.
In the first part of this talk, I present NetKAT, a language for expressing
network-wide packet-forwarding policies. NetKAT comes equipped with a
denotational semantics and a sound and complete equational theory drawn from a
well-studied mathematical structure called a Kleene algebra with tests (KAT).
The equational theory has many practical applications, such as syntactic
techniques for checking reachability and proving non-interference properties
that ensure isolation between policies. Here, I focus on applying the
equational theory to guide and establish the correctness of a compilation
algorithm targeting switches that expose simple, single-table packet-processing
In the second part of this talk, I show how to extend the switch-specific
fragment of NetKAT with operators for writing and deploying network policies to
switches with multiple-table, reconfigurable packet-processing pipelines. The
language, called Concurrent NetCore, allows a network programmer to specify a
virtual packet-processing pipeline, an abstraction that captures the physical
resources required by the controller and also hides the details of the
(potentially varied) pipelines of switches in the network.
I also show how to use Concurrent NetCore to model the pipelines of three
switching architectures and present compilation algorithms for mapping
arbitrary virtual pipelines---and arbitrary packet-processing policies---to the
physical pipelines. Along the way, I explore metatheoretical properties of the
language and present correctness proofs for the compilation algorithms.
Together, these abstractions and compilation algorithms pave the way for
easier fine-grained network management.
This talk draws on joint work with Carolyn Jane Anderson, Nate Foster, Michael
Greenberg, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, and David Walker.
More information about the talks