Network Configuration Verification & Repair

Many 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 and correct control plane behavior under arbitrary link failures.

Abstract Representation for Control Planes

State-of-the-art control plane verifiers are either too slow or impractical to use for verification tasks. We have created 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. We have developed algorithms to automatically derive a network's ARC from its configuration files and formally formally proven ARC's usefulness in proactive analysis under arbitrary failures. Our evaluation over 300+ production data center networks has shown 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.

Control Plane Repair (CPR)

Inspired by recent work in automatic program repair, we introduce CPR, a system that automatically computes correct, minimal repairs for network control planes. CPR casts configuration repair as a MaxSMT problem whose constraints are based on a digraph-based representation of a control plane's semantics. Crucially, this representation captures the dependencies between traffic classes arising from the cross-traffic-class nature of control plane constructs. The MaxSMT formulation accounts for these dependencies whilst also accounting for all policies and preferring repairs that minimize the size (e.g., number of lines) of the configuration changes. Using configurations from 96 production data center networks, we show that CPR produces repairs in less than a minute for 98% of the networks, and these repairs require changing the same or fewer lines of configuration than hand-written repairs in 79% of cases.