Switch as a Verifier: Toward Scalable Data Plane Checking via Distributed, On-Device Verification
Data plane verification (DPV) is important for finding network errors. Current DPV tools employ a centralized architecture, where a server collects the data planes of all devices and verifies them. Despite substantial efforts on accelerating DPV, this centralized architecture is inherently unscalable. In this paper, to tackle the scalability challenge of DPV, we circumvent the scalability bottleneck of centralized design and design Coral, a distributed, on-device DPV framework. The key insight of Coral is that DPV can be transformed into a counting problem on a directed acyclic graph, which can be naturally decomposed into lightweight tasks executed at network devices, enabling scalability. Coral consists of (1) a declarative requirement specification language, (2) a planner that employs a novel data structure DVNet to systematically decompose global verification into on-device counting tasks, and (3) a distributed verification (DV) protocol that specifies how on-device verifiers communicate task results efficiently to collaboratively verify the requirements. We implement a prototype of Coral. Extensive experiments with real-world datasets (WAN/LAN/DC) show that Coral consistently achieves scalable DPV under various networks and DPV scenarios, i.e., up to 1250 times speed up in the scenario of burst update, and up to 202 times speed up on 80% quantile of incremental verification, than state-of-the-art DPV tools, with little overhead on commodity network devices.
Code (0)
등록된 구현이 없습니다.
Methods 이 논문이 사용한 방법론
Similar Papers 제목 키워드 기반
Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes
Recently, cutting-plane methods such as GCP-CROWN have been explored to enhance neural network verifiers and made significant advances. However, GCP-CROWN currently relies on generic cutting planes (cuts) generated from …
Diagnosing LLM Arbitration Behavior over Pre-evidence Epistemic States in RAG-based Fact-Checking
In RAG-based fact-checking, LLMs are increasingly used as verifiers to check given claims against retrieved evidence. Their parametric knowledge can induce pre-evidence tendencies that may conflict with the retrieved con…
A Certified Proof Checker for Deep Neural Network Verification in Imandra
Recent advances in the verification of deep neural networks (DNNs) have opened the way for a broader usage of DNN verification technology in many application areas, including safety-critical ones. However, DNN verifiers …
Automated Theorem ProvingLEMMAQNNVerifier: A Tool for Verifying Neural Networks using SMT-Based Model Checking
QNNVerifier is the first open-source tool for verifying implementations of neural networks that takes into account the finite word-length (i.e. quantization) of their operands. The novel support for quantization is achie…
QuantizationGeneral Cutting Planes for Bound-Propagation-Based Neural Network Verification
Bound propagation methods, when combined with branch and bound, are among the most effective methods to formally verify properties of deep neural networks such as correctness, robustness, and safety. However, existing wo…
GPU