Scalable and Interpretable Overlay Network Checking via Ensemble Verification#

Xinzhe Liu; Yahui Li; Han Zhang; Xia Yin; Xingang Shi; Zhiliang Wang; Gang Ren; Jilong Wang (Tsinghua University); Jiangyuan Yao (Hainan University)

• Why: Overlay/underlay is the architecture of modern WANs (cloud backbones, telco SD-WAN, service overlays), and control-plane verification tools built for flat underlays choke on it. This is the first verifier purpose-built for overlay/underlay — and it has a real nationwide deployment behind it.
• What: MEV, a control-plane verifier for overlay/underlay networks using a novel "ensemble verification" paradigm: independent reasoning within each routing instance/protocol and within each virtual network, then composition. Deployed on FITI (Tsinghua's nationwide testbed), where it found 22 real misconfigurations that could cause isolation and reachability issues; achieves up to 10²× speedup over an extended Batfish on FITI and synthetic networks (from abstract only).
• How: The decomposition into per-instance/per-virtual-network verification is what buys both scalability and interpretability — errors are explained in the routing instance where they occur rather than as a flat cross-product of states.
• Where applicable: Networks running overlay services (VPNs, L2/L3 VPNs, cloud backbone overlays) atop a routed underlay. The deployment is FITI-specific (China's CERNET-derived infrastructure), but the method is general; interpretable counterexamples matter most where operations teams, not verification researchers, consume the output.