Cloudflare Automates Malware Trigger Packet Generation Using Symbolic Execution and Z3 Theorem Prover

From Bytecode to Bytes: Cloudflare Uses Symbolic Execution to Automatically Generate Malware Trigger Packets

Cloudflare has published a technical deep-dive on using symbolic execution and the Z3 theorem prover to automatically reverse-engineer BPF (Berkeley Packet Filter) bytecode used by Linux malware, turning hours of manual analysis into seconds.

The Problem: BPFDoor Malware

BPFDoor is a sophisticated passive Linux backdoor used by China-based threat actors (Red Menshen/Earth Bluecrow) since at least 2021. It hides in BPF socket programs — small bits of executable logic embedded in the Linux kernel that customize how network traffic is processed. The malware remains dormant until it receives a specific magic packet.

Why Manual Analysis Is Hard

• BPF filters can be hundreds of instructions long
• Complex logical jumps make reverse-engineering slow
• Over 100 instructions in some samples make analysis exponentially harder
• Security researchers face a bottleneck: each sample requires hours of manual assembly analysis
• The filter checks specific byte patterns at specific offsets — reconstructing the valid packet is like solving a puzzle

The Solution: Symbolic Execution + Z3

Cloudflare approach:

1. Symbolic execution: Treat BPF code as a series of constraints rather than just instructions
2. Z3 theorem prover: Work backward from the malicious filter to automatically generate the packet required to trigger it
3. Constraint solving: Z3 solves the system of constraints to produce a valid magic packet

How It Works

• Read the BPF bytecode instructions
• Convert each instruction into a mathematical constraint
• Feed the constraints to Z3 solver
• Z3 outputs the exact bytes needed to satisfy all conditions
• The resulting packet can be used to confirm malware presence and behavior

Results

• Analysis time: Reduced from hours to seconds
• Scalability: Handles complex 100+ instruction BPF programs
• Accuracy: Generates exact trigger packets that match the malware expected input
• Automation: Can be integrated into automated malware analysis pipelines

Why This Matters

This technique has broad implications for security research:

• Faster response: Security teams can analyze new BPF-based malware in seconds instead of hours
• Automated triage: Can be deployed at scale to scan for new BPF malware samples
• Defensive intelligence: Understanding what packets trigger malware helps build network detection rules
• Tool availability: The methodology can be applied to other bytecode analysis challenges

Source: Cloudflare Blog — April 8, 2026