2022/04/22 by Aaron Gember-Jacobson, Gember-Jacobson, Aaron, Ruchit Shrestha +3
Computer Science · #Network Packet Processing and Optimization #VLSI and Analog Circuit Testing #Software-Defined Networks and 5G
paper · pdf · doi:10.48550/arxiv.2204.10785
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.