XNV: Explainable Network Verification

Network verification has recently made strides, focusing on the satisfiability of configurations and policies or the performance and versatility of their methods. However, they generally ignore explainability, which is the ability to explain why a network violates or satisfies a certain forwarding policy. In this paper, we propose an explainable network verification framework XNV, which uses a novel interpretable fault analysis method to construct an effective explainable network verifier using knowledge graph (KG). XNV provides appropriate explanations to help operators understand the verification results, improving the transparency and trustworthiness of the verification system. First, XNV uses the KG as an intermediate representation of the configuration semantic level, storing the configuration semantics and routing protocol states. Then, XNV constructs human-logical fault trees for policies and implements root-cause analysis of policy violations based on KG queries and minimum cut set matching. Experiments and case evaluations show that our system provides good interpretability while balancing performance, accelerated understanding, and handling of misconfigurations.