Firebolt: Finding Bugs in Programmable Data Plane Generators
summary
Firebolt is a black‑box tester that generates syntax-guided intent generation from a generator’s BNF plus semantic constraints, prunes the intent space with intent-space pruning, composes per-symbol specifications into intent specs, formalizes generated P4 programs into three SMT formulas, and checks them with Z3. Running thousands of intents against three open‑source generators (mapper, sonata, poise) produces five security vulnerabilities, several intent violations and one crash, finishes generation and verification within ~25 minutes, and claims ~2× bug yield with 0.01–0.1% of prior manual effort.
AI-written summary · about
chapters (11)
- 0:00Intro
- 0:32Programmable Data Plane Gains Significant Traction
- 1:31Data Plane Generators Make Programming Easier
- 2:03Understanding the Correctness of DP Generators
- 4:03Firebolt Workflow
- 5:47Generating Reasonable Intents
- 9:32Generating Representative Intents
- 12:15Deriving Specifications Automatically
- 17:08Bug Coverage
- 17:30Scalability
- 18:46Conclusion
related talks
22mP4-Based Automated Reasoning (P4-BAR) using Symbolic Execution
12mMetha: Network Verifiers Need To Be Correct Too!
25mP4-SpecTec: A Language Mechanization Framework for P4
01h 01mNetwork Verification: Past, Present, and Future
21mParDiff: Practical Static Differential Analysis of Network Protocol Parsers
16mBluetooth Low Energy Security Testing with Combinatorial Methods
22mDependently-Typed Data Plane Programming
10mFuzzBT: Holistic-State-Guided Fuzzing for Bluetooth Host Stack in Kernels