From bytecode to bytes: automated magic packet generation

Linux malware often hides in Berkeley Packet Filter (BPF) socket programs, which are small bits of executable logic that can be embedded in the Linux kernel to customize how it processes network traffic. Some of the most persistent threats on the Internet use these filters to remain dormant until they receive a specific "magic" packet. Because these filters can be hundreds of instructions long and involve complex logical jumps, reverse-engineering them by hand is a slow process that creates a bottleneck for security researchers.

To find a better way, we looked at symbolic execution: a method of treating code as a series of constraints, rather than just instructions. By using the Z3 theorem prover, we can work backward from a malicious filter to automatically generate the packet required to trigger it. In this post, we explain how we built a tool to automate this, turning hours of manual assembly analysis into a task that takes just a few seconds.

Before we look at how to deconstruct malicious filters, we need to understand the engine running them. The Berkeley Packet Filter (BPF) is a highly efficient technology that allows the kernel to pull specific packets from the network Continue reading