Scalable verification for complex networks

Chou, Kuan-Yen

Permalink

https://hdl.handle.net/2142/127193 Copy

Description

Title

Scalable verification for complex networks

Author(s)

Chou, Kuan-Yen

Issue Date

2024-11-15

Director of Research (if dissertation) or Advisor (if thesis)

Godfrey, Philip B

Doctoral Committee Chair(s)

Caesar, Matthew C

Committee Member(s)

• Mittal, Radhika
• Xu, Tianyin
• Walker, David
• Smolka, Steffen

Department of Study

Siebel School Comp & Data Sci

Discipline

Computer Science

Degree Granting Institution

University of Illinois at Urbana-Champaign

Degree Name

Ph.D.

Degree Level

Dissertation

Keyword(s)

• network verification
• configuration verification
• distributed verification
• model checking
• concolic testing
• symbolic execution
• stateful model extraction

Abstract

As computer networks become a foundational modern infrastructure for applications essential to our daily lives, network verification has emerged as a crucial method for ensuring correct network operations through rigorous mathematical analysis. However, while significant advancements in network verification have been proposed in academic literature over the past decade, practical industry adoption has only recently begun, where most verifiers are custom-built for specific networks. Few existing solutions offer general-purpose verifiers capable of handling both the complexity and scale of modern networks. This discrepancy between academic innovation in network verification and their practical adoption stems from inherent scalability limitations in widely used formal verification techniques, such as SMT solving and symbolic execution. These scalability challenges manifest across various abstraction layers, including configuration verification and data plane verification. To circumvent the scalability issues, prior academic solutions often compromise performance or restrict the scope of supported network features to reduce complexity, thus limiting their real-world applicability. This dissertation identifies three core challenges due to this dichotomy between the verification scalability and three different types of complexity of the networks being verified: (1) control plane protocol complexity, (2) data plane complexity, and (3) software implementation complexity. These factors hinder the scalability of network verification and the support for complex networks in practice. To overcome these issues, we propose novel solutions aimed at enhancing verification scalability without sacrificing the ability to handle complex network features, ultimately facilitating the adoption of scalable network verification in practice. Plankton is introduced as a configuration verification system that handles control plane protocol complexity while simultaneously ensuring verification scalability for large network sizes. It combines equivalence partitioning in packet header space with explicit-state model checking and reduces complex control plane protocols to an abstract protocol while preserving soundness. As a result, Plankton exhaustively verifies all possible converged states from a given control plane configuration and surpasses the existing methods by several orders of magnitude in performance, while also accounting for protocol features and potential failures. With increased scale and data plane complexity, the monolithic nature of symbolic network models becomes the bottleneck for data plane verification. To address this, Scylla is proposed as a distributed data plane verifier that efficiently scales data plane verification within varying resource constraints by slicing and distributing the network model. Scylla is the first data plane verifier that slices the network model at the intent granularity and distributes these slices across a compute cluster. This pragmatic design easily scales out for higher numbers of intents and fundamentally changes the scaling of data plane verification from scaling with the network size to scaling with intent slices, thereby enabling scalable data plane verification with minimal computational overhead. Conventional network verification relies on developer input to create models, which is cumbersome and prone to error. As network complexity grows with software implementations like software routers and network functions (NFs), this implementation complexity results in either the lack of models or unreliable verification results due to the use of inaccurate models. To address this, Neo and Mimesis are proposed as solutions with distinct scopes of application. Neo is a hybrid data plane testing framework that combines symbolic model checking with emulation-based testing, achieving network-level concolic testing similar to concolic execution in traditional software analysis. By running software devices as concrete processes on emulators, Neo enhances the applicability and accuracy, though at the potential expense of reduced coverage within emulated software devices. On the other hand, Mimesis offers an automated system for extracting formal models directly from network program binaries. Using full-system symbolic execution and dynamic instrumentation, Mimesis exhaustively captures the packet-forwarding logic of network programs within a configurable bounded depth, and produces models that can assist with network verification. The resulting models, encoded compactly in binary decision diagrams (BDDs), are suitable for real-time verification and compatible with existing verifiers. Mimesis has been demonstrated to work across diverse network programs, including userspace NFs, kernel NFs using raw socket APIs, and eBPF programs. The thesis of this dissertation is to scale verification to large network sizes while supporting the complexity of network features. It tackles the key obstacles for practical network verification by introducing scalable solutions targeted at different dimensions of network complexity. Plankton, Scylla, Neo, and Mimesis provide innovative methods for verifying control plane protocols, data planes, and virtualized networks with software components. These contributions bridge the gap between academic advancements and real-world deployment, enhancing the scalability, accuracy, and applicability of network verification across diverse and complex network environments.

Graduation Semester

2024-12

Type of Resource

Thesis

Handle URL

https://hdl.handle.net/2142/127193

Copyright and License Information

Copyright 2024 Kuan-Yen Chou

Owning Collections