NetSMC: A Custom Symbolic Model Checker for Stateful Network Verification
summary
NetSMC is a custom symbolic model checker that encodes stateful NFs using an existential first-order encoding and analyzes a one-packet-at-a-time model that yields a finite state space. It proves correctness for an order-preserving class of policies, implements a bespoke backward model-checking engine, and scales to hundreds of NFs versus previous tools that handle only tens, achieving roughly 100–200x speedup in benchmarks. Limits: it misses bugs from packet interleavings and supports only a restricted NF operation set.
AI-written summary · about
chapters (15)
- 0:00Intro
- 0:13Network (dataplane) verification
- 1:03But, real networks have stateful network functions
- 2:01Stateful network verification example
- 3:54Stateful network verification is hard!
- 7:44Conditional completeness theorem
- 9:27Existing approach inefficiencies
- 10:47Background on model checking
- 12:15Challenges on applying MC
- 14:16Encoding using Existential FO
- 15:25Evaluation setup
- 16:07Performance on topology zoo
- 16:20Evaluation on custom algorithm
- 16:45Limitations
- 17:15Conclusion
related talks
27mAlembic: Automated Model Inference for Stateful Network Functions
16mAutomatic Parallelization of Software Network Functions
27mNetComplete: Practical Network-Wide Configuration Synthesis with Autocompletion
17mKATch: A Fast Symbolic Verifier for NetKAT
09mAn Intro to Network Service Mesh (NSM) and Its Relationship to Service M...
29mSynthesis of dependable and self-driving communication networks
12mMetha: Network Verifiers Need To Be Correct Too!
15mFormal Methods for Network Performance Analysis