KATch: A Fast Symbolic Verifier for NetKAT
summary
KATch implements NetKAT verification in Scala and replaces exhaustive packet enumeration with symbolic packets, BDD-style relations called SPs that are canonical SP representations allowing hash-consing. It builds automata labeled by SP transitions, checks equivalence by emptiness of the symmetric-difference automaton, and produces symbolic counterexamples when inequivalent. On InternetTopologyZoo benchmarks it moves many reachability and slice-isolation queries from minutes or timeouts to typically well under a second, matching or beating atomic-predicate tools. Artifacts and code are available for reproduction.
AI-written summary · about
chapters (11)
- 0:00KATch and NetKAT intro
- 1:04NetKAT basics and goals
- 2:48NetKAT tools limitations
- 3:51Symbolic packets and speed
- 6:38Why NetKAT is hard
- 8:25Symbolic packet programs
- 10:35Canonical SP and speed
- 11:39Automata with SP transitions
- 12:41Extending NetKAT
- 14:04Symbolic counterexamples
- 14:49Q&A
related talks
18mActive Learning of Symbolic NetKAT Automata
25mNetwork Change Validation with Relational NetKAT
20mStacKAT: Infinite State Network Verification
16mKatra: Realtime Verification for Multilayer Networks
47mDeep Programmability: A New Lens on Networking
20mNetSMC: A Custom Symbolic Model Checker for Stateful Network Verification
18mAPKeep: Realtime Verification for Real Networks
12mMetha: Network Verifiers Need To Be Correct Too!