Modular Control Plane Verification via Temporal Invariants
summary
Timepiece implements a temporal model and an SMT-backed verifier (C library plus harness) that replaces unsafe stable-state modular checks with temporal interfaces checked by base and inductive checks. A soundness theorem proves these checks include all states reachable by simulation. Evaluation runs per-node checks in parallel on a 96-core VM, verifying a 2,000-node fattree in ~2.37 minutes while a monolithic verifier times out at ~80 nodes after 2+ hours; typical per-node checks finish under five seconds.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 2:53Monolithic verification limits
- 3:54Modular verification with interfaces
- 7:45Temporal interfaces for analysis
- 10:34TimePiece implementation
- 11:57Evaluation setup
- 13:44Hijack filtering results
- 15:52Key takeaways and conclusion
- 16:13Q&A
related talks
01h 01mNetwork Verification: Past, Present, and Future
15mOn Temporal Verification of Stateful P4 Programs
23mVeriFlow: Verifying Network-Wide Invariants in Real Time
20mPlankton: Scalable network configuration verification through model checking
18mLiveness Verification of Stateful Network Functions
19mTiramisu: Fast Multilayer Network Verification
28mSafe, Modular Packet Pipeline Programming
20mNetSMC: A Custom Symbolic Model Checker for Stateful Network Verification