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

NSF FMitF Award Number 2219862

Synopsis

Spurred by programmable switches and network interface cards (NICs), the data planes of com- puter 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 re- spect 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 re- search 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 improve educational outcomes we will develop shared interdisciplinary educational materials on formal methods in networking to be deployed in classes at both institutions. To facilitate technology transfer, we will participate in Network Programming Institute (NPI—an institute designed to facilitate academic, governmental and industrial interaction) activities and continue our close collaborations with cloud providers in the Seattle area.

Personnel

Collaborators

Publications

Code

Educational Activities, Outreach, and Broader Impacts

Last modified: Wed Aug 23 09:52:40 EDT 2023