Automated Formal Analysis of Internet Routing Systems

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.