NeTS: Medium: Foundations And Applications Of Modular
Network Verification
NSF NETS Award Number 2312539
PIs Aarti Gupta and David Walker, Princeton University
This website will contain links to data, code, papers, and results
supported by the NSF grant entitled "Nets: Medium: Foundations And
Applications Of Modular Network Verification."
Synopsis
Networks connect us to our online services – our banks, our colleagues
and friends, our work, our school, our travel plans, our government
resources, and so much more. As such, networks are critical
infrastructure, and any downtime is not only costly, but possibly
dangerous. In order to function properly, networks need to be
configured to route information between computers. Unfortunately,
these configurations are large and complicated, and it is easy to make
mistakes while maintaining them. The goal of this project is to
develop new algorithms and tools to identify mistakes in network
configurations before they cause serious harm. More specifically, the
project will explore ways to divide complex modern networks into
smaller components (i.e., modules) for separate but accurate analysis. Doing so will allow sophisticated analysis techniques to scale to the point they may be applied to the world’s largest and most important networks. This project will advance the theory and practice of modular verification of traditional network control planes. Modular reasoning can help network operators abstract away unnecessary details, localize network bugs, confirm the validity of configuration updates, and scale verification to arbitrarily-large networks.
The specific goals are: (1) to develop new theoretical foundations, including models of network behavior, useful abstractions, and expressive specification languages that support sound and efficient modular reasoning; (2) to design and implement algorithmic methods for verification and synthesis of modular network interfaces; and (3) to build a system for reliable modular network management, with support for migration from traditional infrastructure.
Broader Impacts
To increase access to education in computer science, the project will follow Princeton’s verified Departmental Broadening Participation in Computing plan. In particular, the project will support undergraduate research opportunities. To improve educational outcomes, the project will develop shared interdisciplinary educational materials on formal methods to be deployed in classes at the undergraduate and graduate levels.
Personnel
- Aarti Gupta (PI), Princeton
- David Walker (PI), Princeton
- Divya Raghunathan, Princeton
- Dexin Zhang, Princeton
- Andrew Zhao, Princeton
Collaborators
- John Bloch (Undergraduate Summer Researcher), Duke University
Publications
- Buffy: A Formal Language-Based
Framework for Network Performance Analysis. Amir Seyhani, Junyi
Zhao, Aarti Gupta, David Walker, Mina Tahmasbi Arashloo. Draft, June 2024.
- Kirigami, the Verifiable Art of Network Cutting. Tim Alberdingt
Thijm, Ryan Beckett, Aarti Gupta, and David Walker. IEEE/ACM
Transactions on Networking, Volume 32, Issue 3 pp 2447-2462. Print
ISSN: 1063-6692, Online ISSN: 1558-2566. DOI: 10.1109/TNET.2024.3360371,
June 2024. (PDF)
- Modular Control Plane Verification. Tim Alberdingt Thijm. PhD
Thesis, Princeton University. February 2024. (thesis,
FPO slides)
- Modular Control Plane Verification via Temporal Invariants. Timothy Alberdingk Thijm, Ryan Beckett, Aarti Gupta, David Walker. Proceedings of the ACM on Programming Languages, Volume 7, Issue PLDI, 2023.
(PDF)
Code
-
TimePiece tool and experimental data: github
Educational Activities, Outreach, and Broader Impacts
Last modified: Sat Jul 1 11:30:32 EDT 2023