Localizing Router Configuration Errors Using Minimal Correction Sets
Aaron Gember-Jacobson, Ruchit Shrestha, Xiaolin Sun

TL;DR
This paper presents CEL, a novel SMT-based tool that accurately localizes router configuration errors by identifying minimal correction sets, improving network verification and troubleshooting efficiency.
Contribution
CEL introduces a domain-specific MCS enumeration algorithm for precise localization of configuration errors in network routers, addressing limitations of existing verifiers.
Findings
Successfully locates multiple configuration errors in real networks
Identifies all routing-related errors and half of ACL-related errors
Demonstrates efficiency and accuracy in complex network scenarios
Abstract
Router configuration errors are unfortunately common and difficult to localize using current network verifiers. We introduce a novel configuration error localizer (CEL) that precisely identifies which configuration segments contribute to the violation of forwarding requirements. In particular, CEL generates a system of satisfiability modulo theories (SMT) constraints-which encode a network's configurations, control logic, and forwarding requirements-and uses a domain-specific minimal correction set (MCS) enumeration algorithm to identify problematic configuration segments. CEL efficiently locates several configuration errors in real university networks and identifies all routing-related and at least half of all ACL-related errors we introduce.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsNetwork Packet Processing and Optimization · VLSI and Analog Circuit Testing · Software-Defined Networks and 5G
