國立虎尾科技大學 |

Modular Control Plane Verification.

Record Type:	Language materials, manuscript : Monograph/item
Title/Author:	Modular Control Plane Verification./
Author:	Alberdingk Thijm, Timothy Robin.
Description:	1 online resource (186 pages)
Notes:	Source: Dissertations Abstracts International, Volume: 85-10, Section: B.
Contained By:	Dissertations Abstracts International85-10B.
Subject:	Computer science. -
Online resource:	click for full text (PQDT)
ISBN:	9798382193953

Modular Control Plane Verification.
Alberdingk Thijm, Timothy Robin.

Modular Control Plane Verification. - 1 online resource (186 pages)

Source: Dissertations Abstracts International, Volume: 85-10, Section: B.

Thesis (Ph.D.)--Princeton University, 2024.

Includes bibliographical references

Networks continue to experience costly outages due to misconfigured control planes. Avoiding misconfigurations 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 user divides 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 interfaces as 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 change fragments' stable routes. However, if we naively extend Kirigami's interfaces to use overapproximate 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.

Electronic reproduction.
Ann Arbor, Mich. :
ProQuest,
2024

Mode of access: World Wide Web

ISBN: 9798382193953Subjects--Topical Terms:

573171
Computer science.
Subjects--Index Terms:

Automated verificationIndex Terms--Genre/Form:

554714
Electronic books.

Modular Control Plane Verification.
LDR:03548ntm a22004097 4500 001 1150324
005 20241028114746.5
006 m o d
007 cr bn ---uuuuu
008 250605s2024 xx obm 000 0 eng d
020 $a 9798382193953
035 $a (MiAaPQ)AAI30991449
035 $a AAI30991449
040 $a MiAaPQ $b eng $c MiAaPQ $d NTU
100 1 $a Alberdingk Thijm, Timothy Robin. $3 1476787
245 1 0 $a Modular Control Plane Verification.
264 0 $c 2024
300 $a 1 online resource (186 pages)
336 $a text $b txt $2 rdacontent
337 $a computer $b c $2 rdamedia
338 $a online resource $b cr $2 rdacarrier
500 $a Source: Dissertations Abstracts International, Volume: 85-10, Section: B.
500 $a Advisor: Gupta, Aarti.
502 $a Thesis (Ph.D.)--Princeton University, 2024.
504 $a Includes bibliographical references
520 $a Networks continue to experience costly outages due to misconfigured control planes. Avoiding misconfigurations 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 user divides 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 interfaces as 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 change fragments' stable routes. However, if we naively extend Kirigami's interfaces to use overapproximate 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.
533 $a Electronic reproduction. $b Ann Arbor, Mich. : $c ProQuest, $d 2024
538 $a Mode of access: World Wide Web
650 4 $a Computer science. $3 573171
650 4 $a Computer engineering. $3 569006
650 4 $a Information technology. $3 559429
653 $a Automated verification
653 $a Computer networks
653 $a Control planes
653 $a Formal methods
653 $a Modular verification
653 $a Routing
655 7 $a Electronic books. $2 local $3 554714
690 $a 0984
690 $a 0489
690 $a 0464
710 2 $a ProQuest Information and Learning Co. $3 1178819
710 2 $a Princeton University. $b Computer Science. $3 1179801
773 0 $t Dissertations Abstracts International $g 85-10B.
856 4 0 $u http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=30991449 $z click for full text (PQDT)