|Date||May 23, 2017|
|Title||PISCES: A Programmable, Protocol-Independent Software Switch|
Virtualized data-centers use software hypervisor switches to steer packets to and from virtual machines (VMs). The switch frequently needs upgrading and customization---to support new protocol headers or encapsulations for tunneling or overlays, to improve measurement and debugging features, and even to add middlebox-like functions. Software switches are typically based on a large body of code, including kernel code. Changing the switch is a formidable undertaking requiring domain mastery of network protocol design and developing, testing, and maintaining a large, complex code-base. In this talk, we argue that changing how a software switch forwards packets should not require intimate knowledge of its implementation. Instead, it should be possible to specify how packets are processed and forwarded in a high-level domain-specific language (DSL) such as P4, then compiled down to run on the underlying software switch. We present PISCES, a software switch that is not hard-wired to specific protocols, which eases adding new features. We also show how the compiler can analyze the high-level specification to optimize forwarding performance. Our evaluation shows that PISCES performs comparably to Open vSwitch, a hardwired hypervisor switch, and that PISCES programs are about 40 times shorter than equivalent Open vSwitch programs.
Muhammad Shahbaz is a third year Ph.D. student in the Department of Computer Science at Princeton University. His research focuses on the application of software-defined networking (SDN) in campus, enterprise and wide-area networks, network measurement and testing, and language abstractions for programmable data planes. Previously, he worked as a research assistant at the University of Cambridge, Computer Laboratory on the CTSRD and MRC2 projects and was a core member of the NetFPGA-10G project initiated by Stanford University. He received his Bachelor's degree from the Department of Computer Engineering at National University of Sciences and Technology.
|Date||April 18, 2017|
|Title||NetKAT Tutorial: Programming, Modelling, and Reasoning about Networks|
NetKAT is a formal system that can be used to program, model, and reason about networks. It comes with a rich formal toolkit including a sounds and complete algebraic axiomatization; an automata theory; a denotational semantics; and an efficient symbolic representation. These theoretic foundations enable powerful tools such as a decision procedure that allows fully automatic verification of important network properties; and a fast compiler that implements powerful programming abstractions. I will give a tutorial on NetKAT, showing how to use it to program networks and reason about their properties.
Steffen Smolka is a PhD student in Computer Science at Cornell University advised by Nate Foster. Currently his research focuses on languages, tools, and formal foundations for software defined networking. General areas of interest include (probabilistic) semantics, automata theory, and compilers.
|Date||March 14, 2017|
|Title||SNAP: Stateful Network-Wide Abstractions for Packet Processing|
Early programming languages for software-defined networking (SDN) were built on top of the simple match- action paradigm offered by OpenFlow 1.0. However, emerging hardware and software switches offer much more sophisticated support for persistent state in the data plane, without involving a central controller. Nevertheless, managing stateful, distributed systems efficiently and correctly is known to be one of the most challenging programming problems. To simplify this new SDN problem, we introduce SNAP.
SNAP offers a simpler "centralized" stateful programming model, by allowing programmers to develop programs on top of one big switch rather than many. These programs may contain reads and writes to global, persistent arrays, and as a result, programmers can implement a broad range of applications, from stateful firewalls to fine-grained traffic monitoring. The SNAP compiler relieves programmers of having to worry about how to distribute, place, and optimize access to these stateful arrays by doing it all for them. More specifically, the compiler discovers read/write dependencies between arrays and translates one-big-switch programs into an efficient internal representation based on a novel variant of binary decision diagrams. This internal representation is used to construct a mixed-integer linear program, which jointly optimizes the placement of state and the routing of traffic across the underlying physical topology. We have implemented a prototype compiler and applied it to about 20 SNAP programs over various topologies to demonstrate our techniques’ scalability.
Mina is a third-year PhD student in Computer Science at Princeton University, advised by Jennifer Rexford. Her research focuses on designing high-level abstractions for network programming and management, specifically in software defined networks (SDNs).