DPDK Summit 2026

eBPF support was added to DPDK in 2018, enabling users to execute custom byte-code to extend application functionality without rebuilding or restarting. Our Data-Plane team aims to make eBPF a first-class citizen in HC data-plane appliances. However, safe usage requires ensuring custom programs won't crash the application. The current DPDK eBPF verifier lacks essential features and isn't as robust as the Linux kernel version. This presentation covers two aspects:
- eBPF Usage in Data-Plane Appliances: Current and planned uses, missing DPDK eBPF functionality, and requirements for wider community adoption.
- Verifying the Verifier: We applied bounded model checking and deductive verification to verify the BPF validator's correctness. We uncovered multiple previously unknown bugs across distinct classes. For each bug, we produced counterexamples, verified fixes, and machine-checked proofs. Using an AI assistant, we formally verified the validator in days. We'll share practical lessons for applying AI-assisted formal verification to DPDK subsystems.