[1] Genesis : Synthesizing Forwarding Tables in Multi-tenant networks

Paper

Genesis: Synthesizing Forwarding Tables in Multi-tenant Networks, POPL 2017

Paper Abstract

In this work we introduce Genesis, a general and extensible network management system for multi-tenant SDN datacenter networks. Genesis allows rich policies to be specified declaratively and eliminates the need for operators to program the SDN data plane. Prior work for programming SDNs were too low-level, not expressive enough to specify diverse intents (e.g., support for hyperproperties: multiple traffic classes dependent on each other), and were not easily extensible to new intents. We address all these challenges by abstracting the network forwarding behavior and leveraging formal reasoning foundations of constraint solving together with fast SMT solvers to synthesize provably correct switch forwarding tables. Our use of SMT solvers was further motivated by the theoretical complexity of enforcing intents (many intents were NP-complete, for e.g., isolated paths). To make synthesis more tractable, Genesis incorporates a novel search strategy using regular expressions to specify properties which use the structure of datacenter networks, and a divide-and-conquer synthesis procedure which exploits the structure of policy relationships. Our experiments demonstrate we can use Genesis for medium-sized datacenter topologies to enforce a diverse set of intents.

Talks

Slides for talk at POPL

Code

A VM with Genesis installed and instructions to execute it can be found here.

[2] Zeppelin : Synthesis of Fault-Tolerant Distributed Router Configurations

Paper

Zeppelin: Synthesis of Fault-Tolerant Distributed Router Configurations, SIGMETRICS 2018

Paper Abstract

One of the limitations of Genesis was that it was constrained to SDNs, while many networks run ``legacy'' distributed routing protocols like OSPF and BGP because these protocols are scalable and robust to failures. In this ongoing work, we introduce Zeppelin, a tool which can provide support for the intents supported by Genesis to synthesize distributed OSPF and BGP control planes. Since failure handling is distributed in these networks, we augment our synthesis algorithms to provide compliance for intents under small link failures. Zeppelin uses a novel two-phase synthesis approach: (1) it generates paths from intents using Genesis, and then (2) generates intra-domain (shortest-path OSPF) and inter-domain (BGP) router configurations that induce the forwarding state synthesized by Genesis and provide high resilience. For the second phase, we use fast linear programming (LP) solvers and stochastic search to perform better than state-of-art tools which attempt to synthesize control planes directly from intent. Using Zeppelin, we can synthesize highly-resilient and policy-compliant configurations for medium-sized topologies (with 80 routers) 2-3 orders of magnitude faster than state-of-art approaches which synthesize configurations directly from intent.