Date and Time

Tuesday, April 23, 2013 - 12:00pm to 1:30pm

Location

Computer Science 402

Type

Talk

Speaker

Host

Jennifer Rexford

The past twenty years have witnessed significant advances in formal
modeling, system verification and testing of network protocols.
However a long-standing challenge in these approaches is the
decoupling of formal reasoning process and the actual distributed
implementation. This talk presents my thesis work on bridging formal
reasoning and actual implementation in the context of today’s Internet
routing. I will present the Formally Safe Routing (FSR) toolkit, that
combines the use of declarative networking, routing algebra, and SMT
solver techniques, in order to synthesize faithful distributed routing
implementations from verified network models. Next, I will describe
our work on scaling up formal analysis of lnternet-scale
configurations. Our core technique uses a configuration rewriting
calculus for transforming large network configurations into smaller
instances, while preserving routing behaviors. Finally, I conclude
with a discussion of my ongoing and future work, on synthesizing
provably correct network configurations for the emerging Software
Defined Networking (SDN) platforms.