Tim Alberdingk Thijm will present his FPO "Modular Control Plane Verification" on Friday, February 9, 2024 in CS 105 (and Zoom).

Zoom link: https://princeton.zoom.us/j/95302742818

- Reader: David Walker 

- Reader: Ryan Beckett (Microsoft Research)

- Examiner: Maria Apostolaki (ECE)

- Examiner: Zak Kincaid

Please see talk abstract below.  All are welcome to attend.

Abstract:

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

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.