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,
author = {Chen, Yu and Schneider, Tibor and Vanbever, Laurent},
title = {{Causality Analysis in Control Plane Verification}},
booktitle = {CoNEXT-SW '23: Proceedings of the on CoNEXT Student Workshop 2023},
address = {Paris, France},
year = 2023,
month = dec,
publisher = {Association for Computing Machinery},
doi = {10.1145/3630202.3630237},
url = {https://www.research-collection.ethz.ch/bitstream/handle/20.500.11850/643612/main.pdf}
}Research Collection: 20.500.11850/643612