Hydra: Rich and Scalable Functional Verification of eBPF Deployments
TL;DR
Hydra, a verifier for eBPF deployments that reframes verification at the granularity of program graphs, optimizes verification, with each program being efficiently transformed into path summaries that are reused across chains to answer graph-level queries, is presented.
Abstract
Production eBPF deployments now run as deep, dynamically composed chains of programs. Reasoning about the behavior of such chains is critical - e.g., an upstream program may silently overwrite a downstream's routing decision. Existing symbolic-execution verifiers collapse under path explosion when confronted with large programs or the combinatorial space of deployed chains; their helper models, manually developed and incomplete, further erode soundness. We present Hydra, a verifier for eBPF deployments that (i) reframes verification at the granularity of program graphs, (ii) optimizes verification, with each program being efficiently transformed into path summaries that are reused across chains to answer graph-level queries; and (iii) creates accurate helper models, synthesized by LLMs and validated against the kernel via BPF_PROG_TEST_RUN + kcov. Across 12 programs and 27 synthetic program graphs, Hydra correctly verifies every chain with aggregate speedups over a monolithic baseline of at least ~ 80× (up to 1,506×). Its helper models enumerate 2.5-6× more kernel-validated paths per helper than ebpf-se.