Katra: Realtime Verification for Multilayer Networks
Talkat 19th USENIX Symposium on Networked Systems Design and Implementation (NSDI '22) · 2022-04-04..04-06·
summary
Katra implements a new incremental verifier that models packets as a single header copy and uses partial equivalence classes plus a lazy repair of header stacks to avoid exponential blowup from encapsulation and TTL unfolding. It borrows pushdown-system ideas to bound unbounded stacks, integrates with existing fast verifiers, and is implemented and evaluated. Results show 5x–32x speedups for two-header packets, larger gains with more layers and size, and verifies 99.9% of rules for four layers in well under 1 ms.
AI-written summary · about
chapters (14)
- 0:00Intro
- 0:46Dataplane verification is now a critical technology
- 1:08Progress of dataplane verification over time
- 1:46Layering is a fundamental networking primitive
- 2:58How existing incremental dataplane verifiers work
- 4:40The difficulty of analyzing layered networks
- 5:49Example: transformations can explode the ECS
- 7:24Key Innovations with Katra
- 8:18What are partial equivalence classes
- 9:04Example: Tunnel with TTL field
- 12:46Algorithm summary
- 13:15What properties can Katra check?
- 14:05Comparison with finite header unrolling
- 14:57Conclusions & Summary
related talks
17mKATch: A Fast Symbolic Verifier for NetKAT
20mStacKAT: Infinite State Network Verification
25mNetwork Change Validation with Relational NetKAT
19mTiramisu: Fast Multilayer Network Verification
18mAPKeep: Realtime Verification for Real Networks
18mLiveness Verification of Stateful Network Functions
01h 01mNetwork Verification: Past, Present, and Future
18mActive Learning of Symbolic NetKAT Automata