Config2Spec: Mining Network Specifications from Network Configurations
Abstract
Network verification and configuration synthesis are promising approaches to make networks more reliable and secure by enforcing a set of policies. However, these approaches require a formal and precise description of the intended network behavior, imposing a major barrier to their adoption: network operators are not only reluctant to write formal specifications, but often do not even know what these specifications are. We present Config2Spec, a system that automatically synthesizes a formal specification (a set of policies) of a network given its configuration and a failure model (e.g., up to two link failures). A key technical challenge is to design a synthesis algorithm which can efficiently explore the large space of possible policies. To address this challenge, Config2Spec relies on a careful combination of two well-known methods: data plane analysis and control plane verification. Experimental results show that Config2Spec scales to mining specifications of large networks (>150 routers).
Research Area: Verification and Synthesis
People
BibTex
@INPROCEEDINGS{birkner2020configspec,
isbn = {978-1-939133-13-7},
year = {2020},
booktitle = {Proceedings of the 17th USENIX Symposium on Networked Systems Design and Implementation},
type = {Conference Paper},
editor = {Bhagwan, Ranjita and Porter, George},
author = {Birkner, Rüdiger and Drachsler-Cohen, Dana and Vanbever, Laurent and Vechev, Martin},
abstract = {Network verification and configuration synthesis are promising approaches to make networks more reliable and secure by enforcing a set of policies. However, these approaches require a formal and precise description of the intended network behavior, imposing a major barrier to their adoption: network operators are not only reluctant to write formal specifications, but often do not even know what these specifications are. We present Config2Spec, a system that automatically synthesizes a formal specification (a set of policies) of a network given its configuration and a failure model (e.g., up to two link failures). A key technical challenge is to design a synthesis algorithm which can efficiently explore the large space of possible policies. To address this challenge, Config2Spec relies on a careful combination of two well-known methods: data plane analysis and control plane verification. Experimental results show that Config2Spec scales to mining specifications of large networks (>150 routers).},
language = {en},
address = {Berkeley, CA},
publisher = {USENIX Association},
title = {Config2Spec: Mining Network Specifications from Network Configurations},
PAGES = {969 - 984},
Note = {17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 2020); Conference Location: Santa Clara, CA, USA; Conference Date: February 25-27, 2020}
}Research Collection: 20.500.11850/432701