Data plane verification (DPV) can be critical in ensuring the network operates correctly. To be useful in practice, they need to be: (1) fast so as to prevent significant packet loss or security violations; (2) scalable so as to accommodate today's large-scale network architecture. Current DPV tools struggle to meet these requirements due to their centralized architecture. To be concrete, there is a bottleneck for a single-point server to perform real-time DPV tasks. Furthermore, a single-point server makes it hard to collect real-time data plane updates from every device in large-scale networks.

There is an increasing interest in data plane verification, which is designed to automatically verify network correctness through directly analyzing the data plane. Recent data plane verifiers have been able to do real-time sub-millisecond per rule verification. However, we observe that in real-world networks, individual data plane updates rarely occur. On the contrary, there are always a certain number of updates generated in a short period of time, called asburst updates, due to high-level user intend or uncertain network events. When it comes to this real-life scenario, yet, the current equivalence class (EC) based methods are unable to solve themodel-wide changesproblem caused by the EC itself, which significantly slows down the verification speed of burst updates. To overcome this limitation, we present EPVerifier, a fast, scalable data plane verifier accelerating burst updates verification with edge-predicate (EP). Instead of classifying packets into ECs according to global forwarding behavior, the EPVerifier uses one EP per edge to represent all packets that can pass through. Furthermore, with EPs that clearly have localized properties, we introduce a rule type extension that does not require a change in the granularity of the network model to support ACLs and NATs that are prevalent in real devices, and obtain better-performing parallelism by dividing the verification task based on switches. Experiments on both dataset simulations and real-life deployments show that EPVerifier achieves 2-$10\times $faster data plane verification than the state-of-the-art and such advantage expand with the data plane’s complexity and update scale growth.

The data plane verification of networks in hyperscale environments is challenging due to the complexity and size of modern networks. In this paper, we introduce Medusa, a novel verifier that efficiently analyzes large data plane models using parallel processing on multi-core CPUs. First, we propose a new data structure called RANGESET, which overcomes the parallelism limitations of existing popular data structures such as Binary Decision Diagrams (BDD) used in data plane verifiers. Next, we leverage multi-core processing by dividing the network into distinct groups and assigning each group to a separate thread for computation. The results are then integrated for comprehensive verification. By optimizing the use of multi-core systems, we enhance computational efficiency and accelerate the verification process. Experimental results demonstrate that Medusa outperforms existing tools in terms of speed and memory. For instance, in a network with O(10K) devices and O(1M) forwarding rules, Medusa can detect loops in approximately 5 seconds, outperforming other Data Plane Verifiers (DPVs) where some cannot model and analyze the network. Moreover, in networks that we could compare with other state-of-the-art DPVs, Medusa provides a substantial improvement, with speedups up to 600X, 4000X, and 800X compared to alternatives like Flash, APKeep, and Tulkun, respectively.