SyNet: Network-wide Configuration Synthesis

SyNet automatically synthesizes configurations for routers running multiple interacting protocols, including policy-based protocols (BGP) and shortest-path protocols (OSPF), and it also supports static routes. SyNet guarantees that the network's routers converge to a forwarding state that conforms with all high-level requirements provided by the network operator.

SyNet code is released at

Why Multiple Protocols?

Routing protocols have different expressiveness. Configuring multiple protocols is therefore often required to produce a forwarding state compliant with the operator's requirements.

Automatic vs. Manual Configuration

Routing protocols are complex. Moreover, protocols often have complex interdependencies. For example, BGP uses interdomain routing costs as input for selecting the best route. Not surprisingly, the majority of network downtimes are caused by incorrect network configurations.

Which Protocols does SyNet Support?

SyNet currently supports BGP, OSPF, and static routes. SyNet is, however, general and can be extended to support additional routing protocols.

Distributed vs. Static Routing

Relying as much as possible on distributed routing protocols to compute the forwarding state is critical to ensure network reliability and scalability. Static routing would prevent routers from reacting locally upon failure - a key requirement in any network.

Network-wide Configuration Synthesis, CAV 2017. Heidelberg, Germany. July, 2017. (CAV'17 talk)

by Ahmed El-Hassany, Petar Tsankov, Laurent Vanbever, Martin Vechev

Network-wide Configuration Synthesis, arXiv preprint 1611.02537

by Ahmed El-Hassany, Petar Tsankov, Laurent Vanbever, Martin Vechev

Synthesis for Networks Programmability, Program Analysis and Synthesis Course. Spring 2017.

by Petar Tsankov