Network-wide configuration synthesis

DOI10.1007/978-3-319-63390-9_14MaRDI QIDQ2164228zbMATH OpenOpenAlexFDO

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

Publication date 12 August 2022

Full work available at URL https://arxiv.org/abs/1611.02537

Mathematics Subject Classification ID

Network design and communication in computer systems (68M10) Network protocols (68M12)

Abstract: Computer networks are hard to manage. Given a set of high-level requirements (e.g., reachability, security), operators have to manually figure out the individual configuration of potentially hundreds of devices running complex distributed protocols so that they, collectively, compute a compatible forwarding state. Not surprisingly, operators often make mistakes which lead to downtimes. To address this problem, we present a novel synthesis approach that automatically computes correct network configurations that comply with the operator's requirements. We capture the behavior of existing routers along with the distributed protocols they run in stratified Datalog. Our key insight is to reduce the problem of finding correct input configurations to the task of synthesizing inputs for a stratified Datalog program. To solve this synthesis task, we introduce a new algorithm that synthesizes inputs for stratified Datalog programs. This algorithm is applicable beyond the domain of networks. We leverage our synthesis algorithm to construct the first network-wide configuration synthesis system, called SyNET, that support multiple interacting routing protocols (OSPF and BGP) and static routes. We show that our system is practical and can infer correct input configurations, in a reasonable amount time, for networks of realistic size (> 50 routers) that forward packets for multiple traffic classes.

Recommendations

• Genesis: synthesizing forwarding tables in multi-tenant networks
• Synchronization synthesis for network programs
• Automatic synthesis of transiently correct network updates via Petri games
• The synthesis of communication protocols
• Kaki: concurrent update synthesis for regular policies via Petri games

Cited in

(8)

• Using service grammar to diagnose BGP configuration errors
• Resilient capacity-aware routing
• Automatic synthesis of transiently correct network updates via Petri games
• Faster pushdown reachability analysis with applications in network verification
• Kaki: concurrent update synthesis for regular policies via Petri games
• Model checking data flows in concurrent network updates
• Network Synthesis for Distributed Embedded Systems
• Genesis: synthesizing forwarding tables in multi-tenant networks

This page was built for publication: Network-wide configuration synthesis

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2164228)