Localizing Router Configuration Errors Using Minimal Correction Sets

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.