Fine-grained Distributed Data Plane Verification with Intent-based Slicing

TL;DR

Scylla is a distributed data plane verifier that enables fine-grained, scalable verification of large networks by creating and updating intent-based slices at rule-level granularity, reducing resource requirements.

Contribution

It introduces a novel approach to network verification using intent-based slices and distributed models, overcoming memory and scalability limitations of prior monolithic methods.

Findings

Scylla verifies large networks with reduced memory and time.

Distributed, slice-based models improve scalability.

Fast incremental updates enable real-time verification.

Abstract

Data plane verification has grown into a powerful tool to ensure network correctness. However, existing methods with monolithic models have memory requirements tied to network sizes, and the existing method of scaling out is too limited in expressiveness to capture practical network features. In this paper, we describe Scylla, a general data plane verifier that provides fine-grained scale-out without the need for a monolithic network model. Scylla creates models for what we call intent-based slices, each of which is constructed at the rule-level granularity with only enough to verify a given set of intents. The sliced models are retained and incrementally updated in memory across a distributed compute cluster in response to network updates. Our experiments show that Scylla makes the scaling problem more granular -- tied to the size of the intent-based slices rather than that of the overall network. This enables Scylla to verify large, complex networks in minimum units of work that are significantly smaller (in both memory and time) than past techniques, enabling fast scale-out verification with minimal resource requirement.