Hydra: Rich and Scalable Functional Verification of eBPF Deployments
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...