Date of Award

Spring 1-1-2018

Document Type

Dissertation

Degree Name

Doctor of Philosophy (PhD)

First Advisor

Pavol Cerny

Second Advisor

Bor-Yuh Chang

Third Advisor

Nate Foster

Fourth Advisor

Dirk Grunwald

Fifth Advisor

Mooly Sagiv

Abstract

Software-defined networking (SDN) is revolutionizing the networking industry, but even the most advanced SDN programming platforms lack mechanisms for changing the global configuration (the set of all forwarding rules on the switches) correctly and automatically. This seemingly-simple notion of global configuration change (known as a network update) can be quite challenging for SDN programmers to implement by hand, because networks are distributed systems with hundreds or thousands of interacting nodes---even if the initial and final configurations are correct, naïvely updating individual nodes can lead to bugs in the intermediate configurations. Additionally, SDN programs must simultaneously describe both static forwarding behavior, and dynamic updates in response to events. These event-driven updates are critical to get right, but even more difficult to implement correctly due to interleavings of data packets and control messages. Existing SDN platforms offer only weak guarantees in this regard, also opening the door for incorrect behavior. As an added wrinkle, event-driven network programs are often physically distributed, running on several nodes of the network, and this distributed setting makes programming and debugging even more difficult. Bugs arising from any of these issues can cause serious incorrect transient behaviors, including loops, black holes, and access-control violations.

This thesis presents a synthesis-based approach for solving these issues. First, I show how to automatically synthesize network updates that are guaranteed to preserve specified properties. I formalize the network updates problem and develop a synthesis algorithm based on counterexample-guided search and incremental model checking. Second, I add the ability to reason about transitions between configurations in response to events, by introducing event-driven consistent updates that are guaranteed to preserve well-defined behaviors in this context. I propose network event structures (NESs) to model constraints on updates, such as which events can be enabled simultaneously and causal dependencies between events. I define an extension of the NetKAT language with mutable state, give semantics to stateful programs using NESs, and discuss provably-correct strategies for implementing NESs in SDNs. Third, I propose a synchronization synthesis approach that allows correct "parallel composition" of several event-driven programs (processes)---the programmer can specify each sequential process, and add a declarative specification of paths that packets are allowed to take. The synthesizer then inserts synchronization among the distributed controller processes such that the declarative specification will be satisfied by all packets traversing the network. The key technical contribution here is a counterexample-guided synthesis algorithm that furnishes network processes with the synchronization required to prevent any races causing specification violations. An important component of this is an extension of network event structures to a more general programming model called event nets based on Petri nets. Finally, I describe an approach for implementing event nets in an efficient distributed way on modern SDN hardware. For each of the core components, I describe a prototype implementation, and present results from experiments on realistic topologies and properties, demonstrating that the tools handle real network programs, and scale to networks of 1000+ nodes.

Comments

Advisor: Sriram Sankaranarayanan

Share

COinS