Abstract Representation for Control Planes

Modern networks employ complex, and hence error-prone, routing control plane configurations. In many cases, the impact of errors manifests only under failures, leading to devastating effects. Thus, it is important to proactively verify control plane behavior under arbitrary link failures. State-of-the-art control plane verifiers are either too slow or impractical to use for such verification tasks. We propose a new high level abstraction for control planes, ARC, that supports fast control plane analyses under arbitrary failures. ARC can check key invariants without generating the data plane--which is the main reason for current tools' ineffectiveness. This is possible because of the nature of verification tasks and the constrained nature of control plane designs in networks today. We have developed algorithms to derive a network's ARC from its configuration files. We have also formally proven ARC's usefulness in proactive analysis under arbitrary failures. Our evaluation over 300+ networks shows that ARC computation is quick, and that ARC can verify key invariants in under one second in most cases, which is orders-of-magnitude faster than the state-of-the-art.