APKeep: Realtime Verification for Real Networks
summary
APKeep claims real-time verification of real networks by building an expressive modular device model that composes forwarding, ACL, NAT and policy elements, encoding match and rewrite logic with BDDs and maintaining atomic predicates via split/merge/transfer operations. The implementation updates only affected elements and keeps the minimal number of equivalence classes, achieving sub-millisecond per update on real traces and able to verify individual NAT rule updates mostly <1 ms, while other tools run out of memory.
AI-written summary · about
chapters (13)
- 0:00Intro
- 0:34Background
- 1:40Preliminary to Realtime Network Verification
- 3:58Realtime Verification for "Real" Networks
- 5:23Scalability Issue due to Multi-Field Rules
- 7:47The Modular Network Model
- 9:50Equivalence Class in Modular Network Model
- 11:07Initial State without Rules
- 11:53Splitting and Transferring Predicates
- 12:59Merging Predicates
- 14:24System Implementation
- 15:39Evaluation - Verification Speed
- 17:10Conclusion
related talks
18mNetKeeper: Enhancing Network Resilience with Autonomous Network Configuration...
24mReal Time Network Policy Checking Using Header Space Analysis
17mDifferential Network Analysis
23mVeriFlow: Verifying Network-Wide Invariants in Real Time
01h 01mNetwork Verification: Past, Present, and Future
24mAutomatically Correcting Networks with NEAt
25mNetwork Change Validation with Relational NetKAT
16mKatra: Realtime Verification for Multilayer Networks