From bytecode to bytes- automated magic packet generation (opens in new tab)
Classic BPF filters can hide Linux malware until a precisely crafted “magic” packet arrives, but manually reverse-engineering large filters is slow and error-prone. The post presents a symbolic-execution approach using the Z3 theorem prover to model BPF instructions as packet constraints and automatically generate triggering packets. This reduces analysis from hours of manual work to seconds, even for filters exceeding 100 instructions. ## Why BPF Filters Are Difficult to Analyze - Classic BPF is a small, efficient virtual machine used to filter network traffic inside the Linux kernel. - Unlike eBPF, classic BPF has a simple two-register design but can still contain many conditional jumps and packet-offset calculations. - Malware authors exploit BPF because kernel-level filtering can hide traffic from ordinary user-space monitoring tools. - Short programs are manageable manually, but complexity grows rapidly as filters reach 100 or more instructions. - The core problem is determining which packet bytes satisfy the conditions along an accepting execution path. ## BPFDoor as a Practical Example - BPFDoor is a stealthy Linux backdoor associated with cyberespionage campaigns and groups including Red Menshen/Earth Bluecrow. - It uses BPF to inspect incoming traffic without listening on a dedicated open port. - The example filter checks: - IPv6 or IPv4 EtherType. - UDP protocol. - DNS destination port 53. - Fragmentation status for IPv4 packets. - The IPv4 header length when locating the UDP destination port. - The filter contains two paths leading to acceptance: - An IPv6 UDP packet destined for port 53. - A non-fragmented IPv4 UDP packet destined for port 53. - These paths expose the byte offsets and values that a generated packet must satisfy. ## Finding the Shortest Accepting Path - The tool explores the BPF control-flow graph using a queue. - Each queued item records: - The next instruction pointer. - The sequence of instructions already traversed. - Conditional jumps are explored in both directions. - Paths ending in a drop result are discarded, while paths reaching a nonzero return value are recorded as accepting paths. - Breadth-first traversal prioritizes paths with fewer conditions, helping identify the shortest route to acceptance. - Unconditional jumps are followed directly, while conditional branches enqueue true and false destinations in order of path length. ## Turning Paths into Packets - Once accepting paths are identified, each branch condition becomes a constraint on packet contents. - The required byte offsets, widths, and values can be collected from the executed instructions. - Symbolic execution represents these checks as constraints instead of requiring analysts to reason through every instruction manually. - Z3 can then solve the resulting constraint set and produce packet bytes that satisfy the selected accepting path. - This approach is especially useful for large or heavily branched BPF programs where manual packet construction becomes impractical. The recommended workflow is to combine control-flow exploration with symbolic constraint solving: first identify viable accepting paths, then use Z3 to generate packets satisfying their byte-level requirements. This automates a formerly labor-intensive part of malware analysis and makes complex BPF-based backdoors much faster to investigate.