P4-Based Automated Reasoning (P4-BAR) using Symbolic Execution
summary
Google builds an executable P4 spec, runs P4 Symbolic to generate packets, and diff-tests hardware against a P4-runtime simulator (BMv2/BME2) to check data‑plane behavior. The pipeline automatically produces table‑entry–targeted tests (forwarded vs dropped), finds a conservative total of 340+ unique forwarding bugs (liberal count ~1,500), and reports fewer than five known escapes. The system ships since 2020 across deployment roles and significantly reduces manual testing while evolving tests with API changes.
AI-written summary · about
chapters (13)
- 0:00P4-based automated reasoning intro
- 1:07Motivation at Google
- 3:13Goals for new switches
- 5:16Reliability vs feature velocity
- 7:00P4 as machine-readable spec
- 8:26Simplifying switch behavior
- 10:54P4 reasoning for predictability
- 12:21Diff testing simulator vs switches
- 13:23Generating symbolic input packets
- 14:25Symbolic execution in P4 Symbolic
- 15:50Results and impact
- 17:14Summary and future
- 17:56Q&A
related talks
25mP4-SpecTec: A Language Mechanization Framework for P4
15mWhen P4 Meets Run-to-completion Architecture
18mP4Cub: A Little Language for Big Routers
01h 01mNetwork Verification: Past, Present, and Future
19mP4R-Type: A Verified API for P4 Control Plane Programs
15mOn Temporal Verification of Stateful P4 Programs
01h 08mThe Network is the Computer: A Programming Language Perspective
27mPetr4: Formal Foundations for P4 Data Planes