By applying symbolic execution and the Z3 theorem prover to BPF bytecode, we’ve automated the generation of malware trigger packets, cutting analysis time from hours to seconds.

Cloudflare's platform is a leading provider of internet security and performance solutions, offering insights into web security, content delivery, and DNS management. Through documentation, blog posts, and webinars, Cloudflare provides insights into protecting websites and applications from cyber threats and improving performance. Developers and IT professionals can learn about CDN (Content Delivery Network), DDoS mitigation, and firewall configurations to secure and accelerate web traffic.

Cloudflare

Linux malware often uses classic BPF socket programs as stealthy backdoors that stay dormant until receiving a specific 'magic' packet. Manually reverse-engineering these filters is slow and error-prone, especially for programs exceeding 100 instructions. Cloudflare researchers built a tool called filterforge that applies symbolic execution and the Z3 theorem prover to BPF bytecode, automatically tracing all paths leading to an ACCEPT verdict and generating the corresponding trigger packet using scapy. The approach reduces analysis from hours to seconds. The tool is open-sourced on GitHub and demonstrated against a real BPFDoor malware sample.

From bytecode to bytes: automated magic packet generation