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.

Networks are error-prone due to misconfigurations, and it is hard to identify the root causes in the configuration and find a repair due to the size and complexity of networks running distributed routing protocols. Thus, we advocate Automatic Configuration Repair (ACR) to reduce the manual effort. Specifically, we draw some insights from the field of Automatic Software Repair (ASR), crystallize some lessons learned from the real-world repair experience of a large service provider, and propose some directions to realize ACR. Inspired by the generate-and-validate approach from ASR, we propose localize-fix-validate as a possible approach to realize ACR.

When updating router configurations, network operators often attempt to meet a variety of management objectives (e.g., maintaining structural similarity across devices), while also ensuring all forwarding policies are correctly satisfied. Our tool, AED, automates this process. AED models configuration updates as a collection of syntax tree additions and removals, and formulates an innovative system of SMT (Satisfiability Modulo Theory) constraints that encode configurations' structure and interaction with routing algorithms. Operators express management objectives in a high-level language, and AED translates these to "soft" constraints that are maximally satisfied. Evaluations on real and synthetic network configurations show that AED can update networks with tens of routers and hundreds of policies in under a minute, and AED outperforms both hand-crafted updates and state-of-the-art tools in meeting management objectives.

One of the major challenges faced by network operators pertains to whether their network can meet input traffic demand, avoid overload, and satisfy service-level agreements. Automatically verifying if no network links are overloaded is complicated---requires modeling frequent network failures, complex routing and load-balancing technologies, and evolving traffic requirements. We present QARC, a distributed control plane abstraction that can automatically verify whether a control plane may cause link-load violations under failures. QARC is fully automatic and can help operators program networks that are more resilient to failures and upgrade the network to avoid violations. We apply QARC to real datacenter and ISP networks and find interesting cases of load violations. QARC can detect violations in under an hour.

Existing network policy abstractions handle basic group based reachability and access control list based security policies. However, QoS policies as well as dynamic policies are also important and not representing them in the high level policy abstraction poses serious limitations. At the same time, efficiently configuring and composing group based QoS and dynamic policies present significant technical challenges, such as (a) maintaining group granularity during configuration, (b) dealing with network-bandwidth contention among policies from distinct writers and (c) dealing with multiple path changes corresponding to dynamically changing policies, group membership and end-point mobility. In this paper we propose Janus, a system which makes two major contributions. First, we extend the prior policy graph abstraction model to represent complex QoS and dynamic tateful/temporal policies. Second, we convert the policy configuration problem into an optimization problem with the goal of maximizing the number of satisfied and configured policies, and minimizing the number of path changes under dynamic environments. To solve this, Janus presents several novel heuristic algorithms. We evaluate our system using a diverse set of bandwidth policies and network topologies. Our experiments demonstrate that Janus can achieve near-optimal solutions in a reasonable amount of time.