| |
|
|
 |
Computer
Science Department Special Seminar Program Synthesis for Software-Defined Networking Speaker: Jedidiah McClurg, Assistant Professor, Computer Science, University of New Mexico When: TBA Where: TBA Contact: Wim Bohm (bohm@cs.colostate.edu) Abstract: Transient network bugs such as forwarding loops or black holes can cause problems that range from mildly annoying (degraded quality while watching Netflix) to catastrophic (data loss, security breaches, downtime). Software-defined networking (SDN) offers a new level of network programmability, enabling such bugs to be tackled using custom software, but unfortunately, current SDN programming platforms have a key limitation—they lack mechanisms for correctly changing the global configuration (the set of all forwarding rules on the switches). This seemingly-simple notion of global configuration change (known as a network update) can be challenging for SDN programmers to implement, because networks are distributed systems with many interacting nodes—even if the initial and final configurations are correct, naïvely updating individual nodes can lead to bugs in intermediate configurations. Additionally, SDN programs must simultaneously describe both static forwarding behavior, and dynamic updates in response to events. These event-driven updates add further complexity, due to interleavings of data packets and control messages. In this talk, I will present a program synthesis-based approach for addressing these issues. I will first show how to automatically synthesize network updates that are guaranteed to preserve specified properties, via a novel algorithm based on counterexample-guided search and incremental model checking. Next, I will enable reasoning about transitions between configurations in response to events, by introducing event nets, a Petri-nets-based formalism for event-driven network programming. Finally, I will describe an approach for correct “parallel composition” of several event-driven programs (processes): the programmer writes an event net for each process, as well as a declarative specification of paths that packets are allowed to take, and the synthesizer automatically inserts synchronization among the processes such that the specification will be satisfied by all packets. Bio: Jedidiah (Jed) McClurg is an Assistant Professor of Computer Science at the University of New Mexico, and received his Ph.D. from the CUPLV group at the University of Colorado Boulder in 2018. He is currently working on research in synthesis and verification of software-defined network (SDN) programs, but has broad interest in programming languages, formal methods, and networking. His overall goal is to develop tools and techniques to help programmers write better code. His work has appeared in top conferences such as PLDI and CAV, and he received an Outstanding Research Award (2017) and an Outstanding Teaching Assistant Award (2013) from the CU Boulder CS Department. In his free time, Jedidiah enjoys hiking, rock climbing, and unicycling. |