Towards Accessible Model-Free Verification

Despite coming up on two decades of network verification research, verification tooling continues to see limited real-world adoption and outages continue to occur. Relying on interviews with network engineers and our own experience as a large network operator, we ask why. These conversations reveal that the culprit is traditional verification's reliance on hand-crafted network models, which leads to issues with coverage, correctness, maintainability, and fidelity, ultimately hindering practical applicability and adoption.

To address this, we call for the research community to embrace "model-free verification" through network emulation. Recent technology advancements – maturation of orchestration infrastructure and vendor-provided container images – make it possible to leverage emulation to obtain a high-fidelity converged dataplane from actual router control plane code, and then apply established dataplane verification techniques to this extracted state. We prototype such a system with open-source components, and present early results showing this approach can accurately verify configurations previously untestable, paving the way for more robust, practical network verification.