Automatización de la Ingeniería Inversa de Malware BPF con Ejecución Simbólica y Z3

El problema fundamental que aborda este trabajo es la dificultad y el tiempo que consume la ingeniería inversa manual de programas Berkeley Packet Filter (BPF) complejos, especialmente aquellos utilizados por malware para establecer puertas traseras sigilosas en el kernel de Linux. La naturaleza de bajo nivel y la capacidad de los filtros BPF para manipular el tráfico de red antes de que llegue al espacio de usuario, los convierte en una herramienta atractiva para los atacantes que buscan evadir la detección. A medida que la complejidad de estos programas BPF maliciosos aumenta, con cientos de instrucciones y saltos lógicos, el análisis manual se convierte en un cuello de botella significativo para los investigadores de seguridad.

La solución propuesta se basa en la ejecución simbólica, un método que trata el código como un conjunto de restricciones lógicas en lugar de instrucciones secuenciales. Al combinar esta técnica con un solucionador de teoremas como Z3, es posible trabajar hacia atrás desde la condición de 'aceptación' de un filtro BPF para generar automáticamente el paquete de red exacto que lo activaría. Esto transforma un proceso que antes tomaba horas o días de análisis de ensamblador en una tarea que se completa en segundos, mejorando la eficiencia en la identificación y mitigación de amenazas persistentes.

Arquitectura del Sistema

La arquitectura de la herramienta propuesta, 'filterforge', se compone de varios módulos interconectados para lograr la automatización. El proceso comienza con la ingesta del bytecode BPF, que es luego analizado para identificar los posibles caminos de ejecución que conducen a una condición de 'ACCEPT'. Esto se logra mediante un algoritmo de búsqueda de caminos, que explora el grafo de control del programa BPF, manteniendo un registro de las instrucciones ejecutadas y las condiciones encontradas en cada bifurcación.

Una vez que se identifica un camino exitoso (el 'shortest path' a una condición de ACCEPT), este camino se alimenta a un motor de ejecución simbólica. Este motor simula la ejecución del programa BPF, pero en lugar de valores concretos, utiliza variables simbólicas para representar los bytes del paquete de red de entrada. Cada instrucción BPF (como ldh para cargar un halfword, jeq para saltos condicionales, jset para verificar bits) se traduce en una restricción lógica sobre estas variables simbólicas. Por ejemplo, una instrucción jeq #0x800, jt 7, jf 15 se convierte en una restricción EtherType == 0x800 para el camino verdadero.

Estas restricciones se acumulan y se pasan al solucionador de teoremas Z3. Z3, un SMT solver (Satisfiability Modulo Theories), toma estas restricciones y encuentra una asignación de valores concretos a las variables simbólicas (los bytes del paquete) que satisfaga todas las restricciones y, por lo tanto, active la condición de 'ACCEPT'. Finalmente, los valores de bytes concretos generados por Z3 se utilizan con la biblioteca Scapy para construir un paquete de red real, que puede ser utilizado para pruebas o para identificar la presencia del implante en la red.

class BPFPacketCrafter:
    MIN_PKT_SIZE = 64
    LINK_ETHERNET = "ethernet"
    LINK_RAW = "raw"
    MEM_SLOTS = 16

    def __init__(self, ins: list[BPFInsn], pkt_size: int = 128, ltype: str = "ethernet"):
        self.instructions = ins
        self.pkt_size = max(self.MIN_PKT_SIZE, pkt_size)
        self.ltype = ltype

        self.packet = [BitVec(f"pkt_{i}", 8) for i in range(self.pkt_size)]

        self.A = BitVecVal(0, 32)
        self.X = BitVecVal(0, 32)

        self.M = [BitVecVal(0, 32) for _ in range(self.MEM_SLOTS)]

def _execute_ins(self, insn: BPFInsn):
    cls = insn.cls
    if cls == BPFClass.ALU:
        op = insn.op
        src_val = BitVecVal(insn.k, 32) if insn.src == BPFSrc.K else self.X
        if op == BPFOp.ADD:
            self.A = self.A + src_val

Fundamentos Teóricos

La ejecución simbólica, el pilar de esta solución, tiene sus raíces en la investigación académica de la década de 1970, con trabajos pioneros como los de James C. King en 1976 ("Symbolic Execution and Program Testing"). King propuso la idea de ejecutar programas con entradas simbólicas en lugar de concretas para explorar múltiples caminos de ejecución y generar automáticamente casos de prueba. Este concepto ha evolucionado significativamente, especialmente con el advenimiento de los solucionadores SMT (Satisfiability Modulo Theories) modernos.

El uso de Z3, desarrollado por Microsoft Research, es un ejemplo directo de la aplicación de la teoría de la satisfacibilidad booleana (SAT) y sus extensiones (SMT) a problemas de verificación de software y seguridad. Los SMT solvers son capaces de razonar sobre lógicas más ricas que las booleanas puras, incluyendo aritmética de enteros y bit-vectors, lo cual es crucial para modelar operaciones a nivel de bits y bytes que ocurren en programas BPF. La combinación de la exploración de caminos de ejecución (a menudo mediante búsqueda en anchura o profundidad) con la resolución de restricciones simbólicas por un SMT solver es un patrón bien establecido en herramientas de análisis de seguridad y verificación formal, permitiendo la generación de entradas que satisfacen condiciones complejas o alcanzan estados específicos del programa.