Formal Verification of a Software Defined Delay-Tolerant Network

on YouTube ↗25m

" summary

Claims a verified path from a P4 match‑action pipeline to network‑calculus guarantees by building NetQIR, a domain‑specific IR, a compiler from a restricted P4 subset, and Coq mechanizations of semantics and a type system. Coq proves packet‑correctness and a n2n theorem giving flow bounds (example models a 1 ms processing delay per action). Compilation preserves types so the NetQIR proofs apply to compiled P4, proofs are complete in Coq but the system is compiled only and not yet deployed to NASA testbeds.

AI-written summary · about

" chapters (13)

1. 0:00Introduction
2. 1:08Delay-tolerant networks overview
3. 3:17Bundle protocol versions
4. 5:04Software-defined DTN
5. 7:35Network calculus basics
6. 9:02Formalizing P4 pipelines
7. 12:33P4 to network calculus
8. 15:23Formal guarantees with NetQIR
9. 17:28Compilation pipeline
10. 19:35P4 to NetQIR translation
11. 21:00Service curve guarantees
12. 22:08Conclusion
13. 23:10Q&A

" related talks

• 01h 01mNetwork Verification: Past, Present, and FutureNate Foster · PEPM 2020
• 01h 08mThe Network is the Computer: A Programming Language PerspectiveNate Foster · POPL 2024
• 15mOn Temporal Verification of Stateful P4 ProgramsFei He, Delong Zhang, Chong Ye · NSDI '25
• 18mP4Cub: A Little Language for Big RoutersEric Hayden Campbell, Nate Foster, Rudy Peterson, Ryan Doenges, John Chen, Natalie Isak, Calvin Shyu, Parsia Ataei · CPP 2023
• 18mLiveness Verification of Stateful Network FunctionsAditya Akella, Soudeh Ghorbani, Anubhavnidhi Abhashkumar, Farnaz Yousefi, Kausik Subramanian, Kartik Hans · NSDI 2020
• 47mDeep Programmability: A New Lens on NetworkingNate Foster · ICFP 2022
• 22mDependently-Typed Data Plane ProgrammingEric Hayden Campbell, Nate Foster, Mira Mezini, Matthias Eichholz, Matthias Krebs · POPL 2022
• 19mP4R-Type: A Verified API for P4 Control Plane ProgramsPhilipp Haller, Alceste Scalas, Roberto Guanciale, Jens Kanstrup Larsen · OOPSLA 2023