Causality Analysis in Control Plane Verification
Abstract
Control plane verification promises to help operators build reliable networks by reporting a counterexample that violates the specification. However, a single counterexample imposes a major challenge for operators to understand and repair the violation. To improve the usability of control plane verification, we present the first verifier computing the space of all specification violations as a symbolic expression. Our prototype implementation computes the causality between the network routing state and the external routing inputs that induce that state. Describing the space of all violations helps operators address the root cause of the violation, while presenting the space as a symbolic expression allows operators to further manipulate the output to inspect certain aspects of the problem.
People
BibTex
@INPROCEEDINGS{chen2023causality,
isbn = {979-8-4007-0452-9},
copyright = {Creative Commons Attribution 4.0 International},
doi = {10.3929/ethz-b-000643612},
year = {2023-12-08},
booktitle = {CoNEXT-SW '23: Proceedings of the on CoNEXT Student Workshop 2023},
type = {Conference Paper},
institution = {EC and EC},
author = {Chen, Yu and Schneider, Tibor and Vanbever, Laurent},
abstract = {Control plane verification promises to help operators build reliable networks by reporting a counterexample that violates the specification. However, a single counterexample imposes a major challenge for operators to understand and repair the violation. To improve the usability of control plane verification, we present the first verifier computing the space of all specification violations as a symbolic expression. Our prototype implementation computes the causality between the network routing state and the external routing inputs that induce that state.Describing the space of all violations helps operators address theroot cause of the violation, while presenting the space as a symbolicexpression allows operators to further manipulate the output toinspect certain aspects of the problem.},
keywords = {Network verification; Control plane verification; Network analysis},
language = {en},
address = {New York, NY},
publisher = {Association for Computing Machinery},
title = {Causality Analysis in Control Plane Verification},
PAGES = {5 - 6},
Note = {19th International Conference on emerging Networking EXperiments and Technologies (CoNEXT 2023); Conference Location: Paris, France; Conference Date: December 8, 2023; Conference lecture held on December 8, 2023.}
}Research Collection: 20.500.11850/643612