Network-wide Configuration Synthesis
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.
Research Area: Verification and Synthesis
People
BibTex
@INPROCEEDINGS{el-hassany2017network-wide,
isbn = {978-3-319-63389-3},
abbrev_source_title = {LNCS},
doi = {10.1007/978-3-319-63390-9_14},
year = {2017-07},
booktitle = {Computer Aided Verification. 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II},
volume = {10427},
type = {Conference Paper},
editor = {Majumdar, Rupak and Kunčak, Viktor},
journal = {Lecture Notes in Computer Science},
author = {El-Hassany, Ahmed and Tsankov, Petar and Vanbever, Laurent and Vechev, Martin},
issn = {0302-9743},
language = {en},
address = {Cham},
publisher = {Springer},
title = {Network-wide Configuration Synthesis},
PAGES = {261 - 281},
Note = {29th International Conference on Computer Aided Verification (CAV 2017); Conference Location: Heidelberg, Germany; Conference Date: July 24-28, 2017; Paper presented on July 27, 2017.}
}Research Collection: 20.500.11850/261360