Skip navigation
Please use this identifier to cite or link to this item: http://arks.princeton.edu/ark:/88435/dsp01vd66w323c
Title: Modular Control Plane Verification
Authors: Alberdingk Thijm, Timothy Robin
Advisors: Gupta, Aarti
Contributors: Computer Science Department
Keywords: automated verification
computer networks
control plane
formal methods
modular verification
routing
Subjects: Computer science
Issue Date: 2024
Publisher: Princeton, NJ : Princeton University
Abstract: Networks continue to experience costly outages due to misconfigured control planes. Avoidingmisconfigurations is challenging: control planes often use notoriously inscrutable distributed routing protocols. One remedy is control plane verification, which analyzes control planes to uncover violations of desired properties. Unfortunately, most verification tools analyze the entire network at once. Hence, these monolithic tools often do not scale well as networks grow in size and properties increase in complexity, or compromise on the networks and properties they support. To address these limitations, we explore modular control plane verification, where the userdivides their network into fragments to verify independently, and annotates each fragment with an interface. These interfaces summarize each fragment’s routing announcements (a.k.a. routes). We prove that if each fragment guarantees its interface, assuming the interfaces of its neighbors, then properties of the fragments’ routes hold of the monolithic network’s. We present Kirigami, a formal model of network fragments where users specify interfacesas cuts dividing the network into fragments, annotating fragment boundaries with nodes’ stable routes. We define a Satisfiability Modulo Theories (SMT)-based procedure for checking interfaces, implemented as an extension to the NV (monolithic) verification tool. Kirigami’s SMT checks are up to five orders of magnitude faster than NV’s for a range of industrial topologies with synthesized network policies. Unfortunately, Kirigami’s interfaces are not change-resilient if network updates changefragments’ stable routes. However, if we naïvely extend Kirigami’s interfaces to use over- approximate sets of routes instead of exact routes, the resulting verification procedure allows unsound circular reasoning. To prevent circularity, we introduce a new model, Timepiece, where interfaces are defined using temporal invariants inspired by temporal logic. We implement a new SMT-based checking procedure, which scales to verify networks with thousands of nodes in minutes (compared to hours for a monolithic baseline) and allows users to write change-resilient interfaces.
URI: http://arks.princeton.edu/ark:/88435/dsp01vd66w323c
Type of Material: Academic dissertations (Ph.D.)
Language: en
Appears in Collections:Computer Science

Files in This Item:
File Description SizeFormat 
AlberdingkThijm_princeton_0181D_14890.pdf1.34 MBAdobe PDFView/Download


Items in Dataspace are protected by copyright, with all rights reserved, unless otherwise indicated.