Collaborative Research: FMitF: Track I: Specifying and Verifying Network-wide Properties of Dynamic Data Planes

NSF FMitF Award Numbers 2219862, 2219863

Synopsis

Spurred by programmable switches and network interface cards (NICs), the data planes of computer networks are becoming highly dynamic. They now contain mutable state and control logic that allows them to implement complex behaviors that were traditionally housed in a software control plane or application layer, such as routing, failure detection, caching, or data aggregation. The goal of our proposed research is to make these new networks substantially more reliable by developing tools to formally specify and verify network-wide behavior. We plan to explore the use of distributed, event-driven control as a common abstraction to specify both network functionality and behavioral invariants. This abstraction is a general way to represent data plane activity (e.g., packet arrivals), control plane messages (e.g., routing announcements), and application layer events (e.g., installation of a cache entry). It simplifies programming (preliminary results show a 5 to 10x reduction in program size), hides complicated low-level mechanisms such as packet parsers and deparsers, and provides a general vocabulary with which one may specify network-wide behaviors. We will develop a hybrid verification framework to assure engineers that network behavior matches specifications. Static verification will be used to catch bugs before network program changes are deployed. This proactive capability is a significant advantage, but verification would be with respect to abstract models of networks and subject to assumptions about the operating environment. Dynamic verification, via monitors synthesized from the same high-level specifications, complement static verification. Such monitors will be embedded within the running network, monitoring net- work events as they occur, checking that static assumptions hold up, bridging the scaling gap if one exists, and providing defense in depth.

Intellectual Merit

We will enable network engineers to build and verify networks with dynamic data planes. Key research questions include: 1) How does one define a general, expressive, and tractable specification language that applies to behaviors at multiple levels of abstraction (data, control, and application layers)? 2) How does one develop a compiler and run-time verification method that detects viola- tions of such specifications using the limited resources and primitives available on network switches and with low communication overhead? 3) How can we scale static analysis methods and enable verification of large, rich, stateful, dynamic data planes? 4) Can static and dynamic methods be combined to further improve network reliability? While our primary objective is to improve net- work reliability, the algorithms and infrastructure we will develop may contribute broadly to formal methods and find use in other domains.

Broader Impacts

Reliable networks are an essential component of the nation’s critical infrastructure; our research will help keep that infrastructure running and protect it from attack. To increase access to computer science, we will follow Princeton and UW’s verified institutional BPC plans. In particular, we will support Princeton’s summer undergraduate programming experience and UW’s graduate student recruitment. To educate other researchers about our work, we will write about network verification on PI Mahajan's blog netverify.fun among other activities. To facilitate technology transfer, we will continue our close collaborations with cloud providers in the Seattle area.

Personnel

Collaborators

Publications

Invited Talks and Outreach

Open Source Code

Educational Activities

Last modified: Wed Sep 18 11:05:19 EDT 2024