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: Title: Abstractions for Software-defined Networks Abstract: 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 pipelines. 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. Thanks! Cole