Automated Verification of Customizable Middlebox Properties with Gravel
summary
Builds Gravel, a framework that extracts SMT formulas via symbolic execution from unmodified Click elements and verifies element- and system-level properties. Automated study finds 45% of elements verify directly and another 33% after small edits; with five domain-specific optimizations Gravel reaches 66% coverage. Gravel verifies five example middleboxes and 11 RFC-derived properties, requires under 10% code changes, completes checks in under two minutes per box, and shows no measurable performance overhead.
AI-written summary · about
chapters (20)
- 0:00Introduction
- 0:16Metaboxes
- 0:42Implications
- 1:19Formal Methods
- 2:09Project Approach
- 2:39Pushbutton Approach
- 4:01Outline
- 5:49Optimizations
- 6:22Loop and Pointer Balance
- 7:37Container Data Structures
- 8:17Rewriting Data Structures
- 9:17State Concrete
- 10:50High Level Interface
- 11:20Connection Persistent Property
- 11:43Connection Persistent Property Induction
- 13:17Verification Framework
- 14:44Benefits of 2step verification
- 15:44Preventing Bugs
- 16:34Verification Effort
- 17:15Conclusion
related talks
01h 01mNetwork Verification: Past, Present, and Future
12mMetha: Network Verifiers Need To Be Correct Too!
14mEPVerifier: Accelerating Update Storms Verification with Edge-Predicate
21mModular Control Plane Verification via Temporal Invariants
29mSynthesis of dependable and self-driving communication networks
14mEZ-SAVE: Evaluation of Easy-to-Deploy Source Address Validation Policies
20mFirebolt: Finding Bugs in Programmable Data Plane Generators
20mMatchBox: A Semantic Foundation for Data Plane Portability