Resumen Técnico: Heimdall

Enunciado del Problema

Los programas del Filtro Extendido de Paquetes de Berkeley (eBPF) son críticos para las extensiones del kernel de Linux en redes, observabilidad y seguridad. Aunque el verificador de eBPF integrado en el kernel hace cumplir la seguridad de memoria a bajo nivel y la terminación, no logra hacer cumplir propiedades de alto nivel a nivel de fuente, como la disciplina de inicialización, la coherencia del esquema y el manejo de errores. Los autores documentan seis clases de errores a nivel de fuente que se compilan y pasan el verificador del kernel, pero que pueden corromper datos silenciosamente, filtrar información sensible o producir resultados de aplicación incorrectos.

Las vulnerabilidades clave identificadas incluyen:

• Estado no inicializado: Los programas que emiten estructuras residentes en la pila sin inicialización a cero filtran residuos de la pila por CPU, incluidos punteros del kernel y direcciones de retorno suficientes para recuperar los desplazamientos de la Aleatorización de la Disposición del Espacio de Direcciones del Kernel (KASLR).
• Retornos de helpers no verificados: Las funciones de ayuda (por ejemplo, bpf_probe_read_user_str) que fallan a menudo se ignoran, provocando la emisión de datos obsoletos de la pila en lugar de cadenas truncadas.
• Discrepancias de búfer/tamaño: Los desarrolladores que pasan tamaños incorrectos a las funciones de ayuda de salida pueden filtrar campos privados adyacentes que contienen punteros del kernel.
• Discrepancias de gancho/contexto: El uso de estructuras de contexto incorrectas (por ejemplo, __sk_buff en un gancho XDP) conduce a una interpretación errónea de los datos.
• Confusión de tipo/esquema de mapa: Discrepancias entre los tamaños de valores de mapa declarados y los datos reales, o la reinterpretación de resultados de búsqueda de mapas como tipos no relacionados.
• Confusión de firmado/no firmado: Almacenar valores de retorno de helpers firmados (que indican errores) en campos no firmados crea valores positivos grandes espurios utilizados como claves de mapa.

Además, el propio verificador de eBPF tiene vulnerabilidades conocidas (por ejemplo, poda no sólida, validación de contratos faltante) que pueden ser explotadas. La migración a un lenguaje seguro en memoria como Rust podría cerrar estas brechas, pero la reescritura manual es impracticable a escala, y las herramientas de traducción automatizada existentes carecen del rigor necesario para garantizar la equivalencia semántica o la seguridad en el contexto de eBPF.

Metodología: El Pipeline de Heimdall

Heimdall es un pipeline automatizado que traduce programas legacy de libbpf en C a Rust idiomático y seguro de Aya. Emplea un proceso iterativo de cinco etapas que combina Modelos de Lenguaje Grande (LLM), análisis estático y verificación formal:

1. Traducción LLM: Un LLM traduce el código fuente C a Rust utilizando mapeos de la API de Aya, macros de gancho y ejemplos funcionales.
2. Compilación y Verificación del Kernel: El código Rust generado se compila a bytecode de eBPF. Los guardias de lint del compilador (por ejemplo, denegar bloques unsafe no utilizados) y el verificador del kernel verifican la seguridad y corrección básicas. Los errores se retroalimentan al LLM para su reparación.
3. Verificación de Seguridad (Análisis Estático): Un motor de análisis estático personalizado escanea el origen Rust en busca de puertas de escape inseguras que el compilador y el verificador podrían pasar por alto. Esto incluye prohibir reservas de búferes de anillo sin tipo, hacer cumplir la inicialización a cero y requerir el manejo explícito de tipos Result para los retornos de helpers.
4. Ejecución Simbólica: Tanto el binario C original como el binario Rust compilado se cargan en un backend personalizado de eBPF para angr. Este backend modela helpers de eBPF, mapas, relocalizaciones y operaciones atómicas. Realiza ejecución simbólica para explorar todos los caminos factibles, generando fórmulas estructuradas para valores de retorno y efectos secundarios de mapas.
5. Verificación de Equivalencia: Un solucionador basado en Z3 verifica si los programas C y Rust son semánticamente equivalentes. Los autores introducen la Equivalencia Semántica Condicional, que requiere equivalencia solo en entradas que satisfacen las condiciones de seguridad declaradas (por ejemplo, que las llamadas a helpers tengan éxito). Esto permite que la traducción más segura de Rust (que maneja errores o rellena memoria con ceros) se considere equivalente al origen C defectuoso en los caminos donde se activa el error, mientras se verifica que la lógica se preserve en los caminos válidos. Si se encuentra un contraejemplo, se retroalimenta al LLM para una reparación dirigida.

Para apoyar esto, los autores construyeron un backend completo de eBPF para angr, que incluye un cargador ELF, definición de arquitectura, elevador IR VEX y stubs de helpers. También desarrollaron una codificación de cadena ITE personalizada para modelar efectos secundarios de mapas bajo claves simbólicas, capturando la semántica de "última escritura gana".

Contribuciones Clave

• Pipeline de Heimdall: El primer sistema automatizado que traduce programas de producción de eBPF de C a Rust con garantías formales por programa de preservación del comportamiento observable.
• Equivalencia Condicional: Un enfoque de verificación novedoso que valida traducciones que mejoran la seguridad (que se comportan de manera diferente en caminos que activan errores) restringiendo las verificaciones de equivalencia a caminos de ejecución seguros.
• Backend de Ejecución Simbólica de eBPF: Un backend completo de eBPF para angr que modela helpers del kernel, mapas y llamadas de BPF a BPF, permitiendo el razonamiento formal a nivel de bytecode.
• Analizador Estático Safe-Aya: Un motor de políticas que rechaza patrones inseguros de Rust (por ejemplo, búferes de anillo sin tipo, errores de helpers ignorados) que pasan el verificador del kernel.
• Hallazgos de Seguridad: Descubrimiento de fugas de información previamente no reportadas en diez programas de código abierto de eBPF, incluida la recuperación de KASLR mediante residuos de pila y fugas de contenido entre eventos en búferes de anillo.
• Punto de Referencia y Evaluación: Un punto de referencia público de 102 programas de eBPF y una evaluación exhaustiva del pipeline de traducción.

Resultados

El sistema se evaluó en 102 programas de eBPF del mundo real de diversas fuentes (libbpf-tools, libbpf-bootstrap, KEN, Suricata, etc.).

• Tasa de Éxito: Heimdall produjo 96 traducciones formalmente verificadas como equivalentes (94.1%). Las seis restantes fueron parcialmente verificadas (debido a límites de ejecución simbólica) o excedieron los límites de escalabilidad del solucionador.
• Cierre de Errores: En las 96 traducciones verificadas, Heimdall cerró el 100% de las instancias observadas de estado no inicializado, retornos de helpers no verificados y confusión de firmado/no firmado.
• Comparación con Líneas Base: En comparación con agentes LLM de línea base sin el pipeline de Heimdall, Heimdall (Agente) logró una tasa de triple paso del 98% (Compilación, Verificación del Kernel, Seguridad, Equivalencia) frente al 4–12% de las líneas base.
• Sobrecarga de Tiempo de Ejecución: La validación en tiempo de ejecución en 10 programas mostró que las traducciones a Rust generalmente incurrieron en una sobrecarga moderada (media geométrica que oscila entre 0.44× y 3.60× en comparación con C), con la mayoría situándose entre 1.14× y 1.89×.
• Seguridad: Las traducciones eliminaron los patrones inseguros específicos (memoria no inicializada, errores no verificados) que causaron las vulnerabilidades identificadas.

Significancia

El artículo afirma que Heimdall es el primer sistema que automatiza la migración segura en memoria de programas de producción de eBPF con garantías formales por programa de que la migración preserva el comportamiento observable. Aborda la brecha entre las garantías de bajo nivel del verificador del kernel y los requisitos de seguridad de alto nivel de las aplicaciones modernas de eBPF. Al combinar LLMs con verificación formal y análisis estático, Heimdall demuestra que la traducción automatizada puede producir código que no solo es sintácticamente correcto, sino también semánticamente equivalente y libre de clases específicas de errores de seguridad a nivel de fuente que el verificador del kernel no puede detectar. El trabajo establece un nuevo punto de referencia para la migración de eBPF y proporciona una base para construir extensiones de kernel más robustas y seguras en memoria.