💻 computer science

From TinyGo to gc Compiler: Extending Zorya's Concolic Framework to Real-World Go Binaries

Este artículo presenta una extensión del marco de ejecución concolic Zorya para admitir binarios de Go multihilo compilados con el compilador gc estándar, permitiendo la detección de vulnerabilidades del mundo real en proyectos de producción como Kubernetes y Go-Ethereum mediante la restauración de estados de hilo, la neutralización de la preempción en tiempo de ejecución y el empleo de análisis de rutas superpuestas.

Autores originales: Karolina Gorna, Nicolas Iooss, Yannick Seurin, Rida Khatoun, Keith Makan

Publicado 2026-05-06

📖 5 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Karolina Gorna, Nicolas Iooss, Yannick Seurin, Rida Khatoun, Keith Makan

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina que eres un inspector de seguridad tratando de encontrar trampas ocultas en una fábrica masiva y compleja. Esta fábrica es un programa escrito en el lenguaje de programación Go.

Durante mucho tiempo, los inspectores de seguridad tuvieron una herramienta especial llamada Zorya que era excelente para inspeccionar fábricas pequeñas y simples (llamadas "binarios TinyGo"). Pero las fábricas del mundo real utilizadas por grandes empresas como Kubernetes y Ethereum son enormes, caóticas y funcionan con muchos trabajadores (hilos) al mismo tiempo. La antigua herramienta Zorya no podía manejar estas fábricas grandes; se confundía con el ruido y la complejidad.

Este artículo trata sobre actualizar Zorya para que finalmente pueda inspeccionar estas fábricas Go del mundo real con múltiples trabajadores. Así es como lo hicieron, explicado de forma sencilla:

1. El Problema: La "Fábrica Ajetreada"

El compilador estándar de Go (llamado gc) construye software que inicia un equipo completo de trabajadores invisibles (hilos del sistema operativo) solo para gestionar el trabajo. También tiene un "policía de tráfico" (el tiempo de ejecución) que puede detener a cualquier trabajador en cualquier momento para permitir que otro pase primero.

La Vieja Herramienta: Zorya se usaba para inspeccionar fábricas tranquilas con un solo trabajador. Cuando intentaba mirar las fábricas ajetreadas con múltiples trabajadores, no podía entender quién hacía qué ni dónde estaban parados los trabajadores.
El Objetivo: Hacer que Zorya sea lo suficientemente inteligente como para pausar el caos, tomar una instantánea de cada trabajador y luego inspeccionar cuidadosamente el trabajo sin perderse.

2. La Solución: Tres Nuevos Superpoderes

Los autores dieron a Zorya tres nuevos trucos para manejar las fábricas grandes:

La "Instantánea de Viaje en el Tiempo" (Restaurando Estados de Hilos):
Imagina que la fábrica está funcionando a toda velocidad. En lugar de intentar observar a los trabajadores moviéndose en tiempo real (lo cual es demasiado rápido y confuso), la nueva Zorya presiona "pausa", toma una fotografía de alta definición de las manos, herramientas y ubicación de cada trabajador individual, y la guarda. Cuando comienza su inspección, carga estas fotos de nuevo para saber exactamente dónde estaba cada uno antes de empezar. Esto le permite ignorar el caos del "policía de tráfico" y centrarse en el código real.
El "Espejo de Qué-Pasaría-Si" (Análisis de Trayectorias Superpuestas):
Por lo general, cuando un trabajador llega a una bifurcación en el camino, elige un camino y lo recorre. El otro camino se ignora.
- La Vieja Forma: Zorya solo verificaba el camino que el trabajador realmente tomó.
- La Nueva Forma: Zorya crea un "espejo fantasma" de la fábrica. Cuando el trabajador elige el camino izquierdo, Zorya envía a un "trabajador fantasma" por el camino derecho solo por unos pocos pasos. Verifica si ese camino tiene una trampa (como un agujero en el suelo o una herramienta rota) sin caminarlo realmente. Si el fantasma encuentra una trampa, Zorya da la alarma. Esto se llama Copy-on-Write (Copiar al Escribir): solo copia las partes de la fábrica que toca el fantasma, ahorrando una enorme cantidad de energía.
El Detector de "Trampas Silenciosas":
Algunas trampas no hacen un ruido fuerte (como un fallo o un pánico). Por ejemplo, un número podría volverse tan grande que "se envuelve" y se vuelve pequeño nuevamente, rompiendo silenciosamente las matemáticas. Otras herramientas pasan por alto estas porque solo buscan fallos ruidosos. Zorya utiliza un cerebro matemático superinteligente (llamado un solver SMT) para hacer las matemáticas en su cabeza. Puede decir: "Oye, si este número se hace más grande, romperá silenciosamente las matemáticas", incluso si el programa no falla.

3. La Prueba: Encontrando Errores Reales

El equipo probó esta Zorya actualizada en 11 vulnerabilidades de seguridad del mundo real encontradas en software famoso como Kubernetes, Go-Ethereum y CoreDNS. Compararon Zorya con otras herramientas como verificadores estáticos (que leen el código como un corrector gramatical), fuzzers (que lanzan datos aleatorios al software) y otros escáneres de seguridad.

Los Resultados:

Zorya encontró 7 de los 11 errores.
La Victoria "Silenciosa": Uno de los errores que Zorya encontró fue un "desbordamiento de entero silencioso". Fue un error matemático que no hizo fallar el programa ni activó una alarma. Ninguna otra herramienta encontró este error a menos que alguien les hubiera dicho manualmente exactamente qué buscar. Zorya lo encontró automáticamente.
La Compensación: Zorya es más lenta que las herramientas de "lanzar datos aleatorios" (fuzzers). Mientras que un fuzzer podría encontrar un fallo en segundos, Zorya tarda unos 16 minutos en encontrar un error. Sin embargo, Zorya no necesita que un humano escriba un script de prueba específico para cada función; simplemente analiza el archivo binario directamente.

4. La Conclusión

Este artículo muestra que ahora podemos usar inspecciones avanzadas de "trabajadores fantasma" para encontrar profundas y ocultas vulnerabilidades de seguridad en software Go complejo y multihilo. Aunque toma un poco más de tiempo que otros métodos, puede encontrar errores "silenciosos" que otras herramientas pasan por completo, haciendo nuestra infraestructura digital más segura.

En resumen: Enseñaron a un robot de seguridad a pausar una fábrica caótica, tomar una instantánea de los trabajadores y verificar los caminos que nadie más está recorriendo, encontrando con éxito trampas ocultas que anteriormente eran invisibles.

Resumen Técnico: De TinyGo al compilador gc: Extensión del Marco de Ejecución Concolica de Zorya a Binarios Go del Mundo Real

Declaración del Problema

El análisis de seguridad de binarios Go compilados con el compilador estándar gc sigue siendo un desafío significativo. A diferencia de los binarios compilados con TinyGo (que producen ejecutables de un solo hilo con tiempos de ejecución mínimos), los binarios compilados con gc utilizan un tiempo de ejecución complejo que gestiona goroutines, recolección de basura y programación preemptiva a través de múltiples hilos del sistema operativo. Las herramientas de ejecución simbólica existentes (por ejemplo, KLEE, angr, Radius2) están diseñadas principalmente para C/C++ y dependen de representaciones intermedias (IR) de LLVM a las que Go no compila completamente. Además, estas herramientas a menudo fallan al modelar mecanismos específicos del tiempo de ejecución de Go, como la preempción cooperativa/asincrónica, la programación de goroutines y las funciones mapeadas en memoria de VDSO, lo que las hace ineficaces contra binarios Go de producción. Las iteraciones anteriores del marco Zorya se limitaban a binarios TinyGo, dejando un vacío en el análisis de aplicaciones Go del mundo real y multihilo.

Metodología

El artículo presenta una extensión de Zorya, un marco de ejecución concolica que eleva binarios compilados a la representación intermedia P-Code de Ghidra. La extensión permite el análisis de binarios multihilo compilados con gc mediante tres mecanismos técnicos principales:

Restauración de Estado y Programación Multihilo:
- Zorya restaura el estado de todos los hilos del sistema operativo desde volcados de gdb en la inicialización, capturando estados de registros, bases de almacenamiento local de hilo (TLS) y trazas de retorno.
- Los hilos se clasifican (por ejemplo, hilo principal, monitor del sistema, en espera) para facilitar la programación.
- El marco neutraliza la preempción del tiempo de ejecución y emplea una política de programación "solo principal" para el análisis en modo función, restringiendo la ejecución concolica al hilo principal para evitar interrupciones por la recolección de basura o monitores del sistema. Esto permite una exploración continua de funciones a nivel de usuario.
Análisis de Trayectorias Superpuestas con Semánticas de Copia al Escribir (CoW):
- Para abordar la explosión de trayectorias y razonar sobre ramas no tomadas sin bifurcar todo el estado (lo cual puede exceder 1 GiB para binarios gc), Zorya implementa un mecanismo de superposición.
- Cuando una rama condicional involucra variables simbólicas rastreadas, se crea una superposición ligera para la ruta no tomada. Las lecturas consultan primero la superposición, recurriendo al estado base en caso de fallo; las escrituras van exclusivamente a la superposición.
- Esta superposición ejecuta un número acotado de instrucciones (predeterminado $N=15$ ) antes de ser descartada, permitiendo la detección de vulnerabilidades en rutas no tomadas por la traza concreta.
Detección de Vulnerabilidades mediante Rutina Analizadora:
- El marco ejecuta instrucciones con valores concretos (del volcado de gdb) y expresiones simbólicas (gestionadas por el solucionador SMT Z3).
- Una "Rutina Analizadora" verifica patrones de vulnerabilidad en cada instrucción, incluyendo desreferencias de punteros nulos, desbordamientos enteros y división por cero.
- Para binarios gc, el sistema aprovecha tanto la exploración de AST (para localizar llamadas explícitas a pánico) como la ejecución superpuesta (para detectar vulnerabilidades silenciosas que no desencadenan pánicos del tiempo de ejecución).

Contribuciones Clave

Extensión a Binarios gc: El marco se extiende para analizar binarios multihilo producidos por el compilador Go estándar, cerrando la brecha entre herramientas de investigación y software Go de producción.
Conjunto de Datos de Vulnerabilidades del Mundo Real: Los autores curaron un corpus de 11 vulnerabilidades reales de proyectos de producción (incluyendo Kubernetes, Go-Ethereum y CoreDNS), completos con flujos de trabajo de reproducción e inputs desencadenantes.
Evaluación Comparativa: Zorya fue evaluado frente a siete herramientas de vanguardia (tres analizadores estáticos, dos fuzers y dos ejecutores simbólicos a nivel de binario).
Detección de Vulnerabilidades Silenciosas: El marco detecta con éxito vulnerabilidades que no desencadenan pánicos del tiempo de ejecución, específicamente desbordamientos enteros silenciosos, sin requerir oráculos escritos manualmente.

Resultados

La evaluación se realizó sobre 11 vulnerabilidades del mundo real en tres clases: desreferencias de puntero nulo, desbordamientos enteros e índices fuera de límites.

Tasa de Detección: Zorya detectó 7 de 11 vulnerabilidades.
- 4 fueron capturadas por la Rutina Analizadora en la ruta concreta (tomada).
- 3 fueron identificadas mediante alcanzabilidad de pánico en AST en la rama no tomada.
- 2 hallazgos secundarios surgieron mediante ejecución superpuesta en rutas no tomadas (detectados dentro del límite de profundidad de 15 instrucciones).
Detección Única: Zorya fue la única herramienta en detectar un desbordamiento entero silencioso en la función memoryGasCost de Go-Ethereum (v1.6.0). Este error implica una multiplicación que envuelve silenciosamente en la aritmética sin signo de Go, permitiendo a un atacante asignar memoria masiva por gas casi cero. Ninguna otra herramienta evaluada encontró este error sin un oráculo escrito manualmente.
Comparación de Herramientas:
- Analizadores Estáticos (staticcheck, gosec, nilaway): Detectaron 0 de los 11 errores. gosec pasó por alto desbordamientos aritméticos del mismo tipo, y nilaway falló en paquetes de Kubernetes debido a problemas de resolución de dependencias.
- Fuzers (go test -fuzz, GoLibAFL): Detectaron 5 de los 11 errores (incluyendo kube-sm-2025, que Zorya perdió debido al agotamiento de recursos en la ejecución simbólica de runtime.memmove). Los fuzers fueron más rápidos (promedio de ~0.18s a 7s) pero requerían harnesses escritos manualmente y pasaron por alto vulnerabilidades silenciosas que no provocan fallos.
- Otros Ejecutores Simbólicos (BINSEC, SymQEMU): Detectaron 0 de los 11 errores, principalmente debido a la falta de soporte para primitivas del tiempo de ejecución de Go.
Rendimiento: Zorya promedió 16.5 minutos por detección, significativamente más lento que los fuzers, pero proporciona una traza completa de ejecución a nivel de instrucción y opera totalmente automáticamente sin harnesses.

Significado y Afirmaciones

El artículo afirma que Zorya aborda un vacío crítico en el panorama de seguridad de Go. Mientras que los analizadores estáticos fallan al razonar sobre aritmética y aliasing específicos del programa, y los fuzers requieren harnesses manuales y pasan por alto errores que no provocan fallos, Zorya ofrece un análisis automático a nivel de binario capaz de detectar vulnerabilidades silenciosas.

Los autores posicionan a Zorya como una herramienta que combina exploración de superposiciones de alta granularidad, recuperación de estado inicial multihilo y detección de desbordamientos silenciosos específicamente para binarios Go. El trabajo demuestra que la ejecución concolica puede adaptarse al tiempo de ejecución complejo y multihilo del compilador Go estándar, permitiendo la detección de vulnerabilidades (como desbordamientos enteros silenciosos) que son invisibles para otras herramientas evaluadas. El artículo concluye que, aunque Zorya es más lento que la fuzzing, su capacidad para proporcionar trazas exactas a nivel de instrucción y detectar errores que no provocan fallos lo convierte en un valioso añadido al conjunto de herramientas de ingeniería de seguridad de software.