Network Change Validation with Relational NetKAT
summary
Relational NetKAT is a specification language for change-by-trace: programs describe a trace relation R and compile it to NetKAT transducers and automata so K_old ◁ R ?= K_new. Naive projection makes packet configurations explicit and induces a ≥2^32 blowup; the compiler instead splits configurations by how much packets differ, keeping packet space symbolic and avoiding the 2^32 expansion. Implementation integrates BDDs, derivatives, and Batfish input, reproduces Batfish tutorial cases under 30s and matches REA’s benchmarks with average times below 1s (naive approach times out).
AI-written summary · about
chapters (12)
- 0:00Introduction
- 1:49Traditional verification limits
- 3:15Relational network verification
- 4:19Relational NetKAT design
- 7:11Atomic constructs
- 9:20Trace relations for changes
- 11:05Compilation challenges
- 14:19Changes are small
- 15:22Performance benchmarks
- 17:49RELA vs Batfish
- 18:10Key takeaways
- 18:33Q&A
related talks
17mKATch: A Fast Symbolic Verifier for NetKAT
18mActive Learning of Symbolic NetKAT Automata
20mStacKAT: Infinite State Network Verification
16mKatra: Realtime Verification for Multilayer Networks
18mAPKeep: Realtime Verification for Real Networks
47mDeep Programmability: A New Lens on Networking
18mNetKeeper: Enhancing Network Resilience with Autonomous Network Configuration...
17mDifferential Network Analysis