Liveness Verification of Stateful Network Functions
summary
Provides a one-big-switch abstraction that programs stateful firewalls, IDS and UDP-flood mitigators, compiles those programs to P4, and verifies liveness by encoding rules as packet-list Boolean formulas. Claims verification is faster—about 8x speedup versus packet-based approaches on examples up to 100 hosts—and scales to a university data center trace (≈100k packets, 1,800 IPs). Compiler emits data-plane/control code in a few milliseconds and runtime overhead is modest (controller calls 0–0.3%).
AI-written summary · about
chapters (10)
- 0:00Introduction
- 0:47Network Verification
- 1:59Liveness Properties
- 2:57Challenges
- 3:46Overview
- 4:22One Big Huge abstraction
- 8:38Packet Less Models
- 9:15Properties
- 11:05Counter Semantics
- 11:43Overhead
related talks
01h 01mNetwork Verification: Past, Present, and Future
15mOn Temporal Verification of Stateful P4 Programs
47mDeep Programmability: A New Lens on Networking
01h 08mThe Network is the Computer: A Programming Language Perspective
25mFormal Verification of a Software Defined Delay-Tolerant Network
16mSequence Abstractions for Flexible, Line-Rate Network Monitoring
23mVeriFlow: Verifying Network-Wide Invariants in Real Time
29mSwitchLog: A Logic Programming Language for Network Switches