ACORN: Network Control Plane Abstraction using Route Nondeterminism

TL;DR

ACORN introduces a scalable approach for verifying distributed network control planes by using abstractions with route nondeterminism and symbolic graph encodings, significantly improving verification speed and capacity.

Contribution

This paper presents a hierarchy of abstractions with route nondeterminism and a novel SMT encoding, enabling scalable formal verification of large distributed network control planes.

Findings

Speedups up to 323x in verification performance

Scales to approximately 37,000 routers in FatTree topologies

Outperforms existing control plane verification tools

Abstract

Networks are hard to configure correctly, and misconfigurations occur frequently, leading to outages or security breaches. Formal verification techniques have been applied to guarantee the correctness of network configurations, thereby improving network reliability. This work addresses verification of distributed network control planes, with two distinct contributions to improve the scalability of formal verification. Our first contribution is a hierarchy of abstractions of varying precision which introduce nondeterminism into the route selection procedure that routers use to select the best available route. We prove the soundness of these abstractions and show their benefits. Our second contribution is a novel SMT encoding which uses symbolic graphs to encode all possible stable routing trees that are compliant with the given network control plane configurations. We have implemented our abstractions and SMT encodings in a prototype tool called ACORN. Our evaluations show that our abstractions can provide significant relative speedups (up to 323x) in performance, and ACORN can scale up to $\approx37,000$ routers (organized in FatTree topologies, with synthesized shortest-path routing and valley-free policies) for verifying reachability. This far exceeds the performance of existing tools for control plane verification.