StacKAT: Infinite State Network Verification
summary
Defines StacKAT, a packet-language that adds a single variable-size stack payload with push/pop to NetKAT-style programs and proves program equivalence decidable by an NFA-based reduction that turns programs into NFAs, cancels matching push/pop edges, intersects with poppush, and runs a synchronized inward-out normalization. Equivalence is PSPACE-complete without header fields and EXPSPACE-complete with headers. A prototype verifier produces counterexamples, runs quickly on stack-only cases but slows with concrete headers; a complete axiomatization (with one bulky axiom) is also given.
AI-written summary · about
chapters (10)
- 0:00StacKAT introduction
- 1:46NetKAT limitations
- 3:31Modeling state with stacks
- 5:35Core language and operations
- 8:08Verification challenges
- 10:55Tool architecture
- 13:41Automaton transformation
- 15:50Complexity and future work
- 17:14Summary and open problems
- 17:36Q&A
related talks
17mKATch: A Fast Symbolic Verifier for NetKAT
16mKatra: Realtime Verification for Multilayer Networks
25mNetwork Change Validation with Relational NetKAT
41mConcatenative programming and stack-based languages
18mLiveness Verification of Stateful Network Functions
47mDeep Programmability: A New Lens on Networking
18mSuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-Based, and SAT(…)
18miStack: A General and Stateful Name-based Protocol Stack for Named Data Networking