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.