VUPER: Verified ASN.1 UPER Parser
Este artículo presenta VUPER, un marco de trabajo que genera analizadores y serializadores ASN.1 UPER formalmente verificados y de precisión de bits, los cuales fueron utilizados para descubrir 20 tipos de inconsistencias y vulnerabilidades de seguridad concretas en analizadores populares, tanto de código abierto como comerciales, mediante pruebas dinámicas en protocolos 5G y V2X.
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 el internet y nuestros teléfonos móviles son una ciudad enorme y bulliciosa donde miles de millones de mensajes viajan entre edificios cada segundo. Para que esta ciudad funcione, estos mensajes necesitan un lenguaje universal para que un teléfono en Nueva York pueda hablar con una torre en Tokio sin confundirse. Este lenguaje se llama ASN.1, y es como la gramática y el vocabio que le dicen a las computadoras exactamente cómo empaquetar la información en cajas digitales diminutas y eficientes. Pero aquí está la parte difícil: para ahorrar espacio y ganar velocidad, estas cajas se empaquetan tan apretadamente que ni siquiera están alineadas con filas ordenadas de bytes (como las palabras estándar de una computadora); en su lugar, se empaquetan hasta el último bit, la partícula más pequeña de datos. Este método específico de empaquetado súper apretado se llama UPER.
El problema es que escribir un traductor (o "parser") para desempaquetar estas diminutas cajas a nivel de bit es increíblemente difícil. Si el traductor comete incluso un error minúsculo —como leer mal un solo bit o olvidar una regla sobre cómo manejar información nueva y desconocida— puede hacer que todo el sistema colapse, filtre secretos o permita que los hackers se cuelen. Durante años, los ingenieros han intentado solucionar estos errores probando los traductores con millones de mensajes aleatorios, con la esperanza de detectar los fallos; pero esto es como intentar encontrar una aguja en un pajar simplemente sacudiendo el paja: podrías encontrar algunas agujas, pero nunca podrás estar seguro de haber encontrado todas o de si las que encontraste son realmente las auténticas.
Aquí entra VUPER, una nueva herramienta creada por investigadores de la Universidad Estatal de Pensilvania que cambia las reglas del juego. En lugar de solo sacudir el pajar, VUPER construye un traductor matemáticamente perfecto desde cero. Piensa en ello como crear un diccionario y un libro de gramática "estándar de oro" que un matemático computacional ha demostrado ser 100% correcto. Los investigadores utilizaron este traductor perfecto para probar otros 11 parsers populares utilizados en redes 5G reales y sistemas de comunicación de vehículos. Descubrieron que muchos de estos traductores ampliamente utilizados eran en realidad bastante no conformes, omitiendo 20 tipos diferentes de reglas. En algunos casos, esta falta de conformidad permitió que los hackers colapsaran teléfonos o engañaran a las redes para que enviaran mensajes sin cifrar. VUPER demuestra que, aunque no siempre podemos confiar en los traductores que tenemos, ahora podemos construir unos que estén matemáticamente garantizados para ser seguros, y usarlos para arreglar los que están rotos.
La historia de VUPER: Construyendo el traductor perfecto
En el mundo de las redes informáticas, los datos son como un largo flujo de agua que corre a través de tuberías. Para enviar un mensaje, una computadora "serializa" la información, exprimiendo los datos en un flujo compacto de bits. Para recibirlo, otra computadora "analiza" (parse) el flujo, exprimiendo los bits de nuevo en un mensaje legible. En el mundo de alto riesgo de las redes celulares 5G y la comunicación vehículo-a-todo (V2X), este proceso utiliza un conjunto específico de reglas llamado UPER (Reglas de Codificación Empaquetadas No Alineadas). Se llama "no alineado" porque no le importan los límites de bytes ordenados; empaqueta los datos lo más apretadamente posible, bit a bit, para ahorrar ancho de banda.
El desafío es que el libro de reglas oficial de UPER está escrito en un texto descriptivo denso, no en código. Esto deja a los ingenieros adivinando cómo implementar las reglas, lo que conduce a errores sutiles. Los investigadores detrás de VUPER decidieron dejar de adivinar. Construyeron un marco que demuestra formalmente que el parser es correcto. No se limitaron a escribir código y esperar que funcionara; utilizaron una poderosa herramienta matemática llamada el probadore Rocq para verificar cada paso de la lógica.
La prueba del "Viaje de Ida y Vuelta" (Round-Trip)
Para entender cómo funciona VUPER, imagina que tienes un traductor mágico que convierte un libro en un código secreto y viceversa. Una prueba de "viaje de ida y vuelta" significa que tomas una oración, la conviertes en código y luego conviertes ese código de nuevo en una oración. Si obtienes exactamente la misma oración, el traductor está funcionando.
Sin embargo, UPER tiene un giro especial: las extensiones. A medida que la tecnología evoluciona (como al pasar de 4G a 5G), se añaden nuevas funciones a los mensajes. Un traductor antiguo debe ser capaz de leer un mensaje nuevo, ignorar las partes nuevas que no entiende y, aun así, dar sentido a las partes antiguas. Esto se llama compatibilidad hacia adelante (forward compatibility). VUPE maneja esto demostrando dos cosas:
- Viaje de ida y vuelta estricto: Si el mensaje es de la misma versión, el traductor debe convertirlo de nuevo en el exacto mismo patrón de bits. Sin bits extra, sin bits faltantes.
- Viaje de ida y vuelta débil: Si el mensaje tiene extensiones nuevas y desconocidas, el traductor puede saltárselas, pero aún debe ser capaz de convertir las partes conocidas de nuevo en un mensaje válido. No tiene que coincidir bit por bit con el original (porque las partes desconocidas ya no están), pero no debe corromper el resto.
Encontrando los errores (Bugs)
Los investigadores construyeron un "oráculo confiable" —un parser perfecto generado por VUPER— y lo usaron para probar otros 11 parsers. Estos incluían 7 herramientas de código abierto (como asn1c y pycrate) y 4 parsers comerciales utilizados dentro de estaciones base reales de 4G y 5G (el hardware que conecta tu teléfono a la red).
No enviaron basura aleatoria; utilizaron un "fuzzer" inteligente que comprendía la estructura de los mensajes para crear millones de casos de prueba complicados. Al comparar los resultados, encontraron 20 tipos diferentes de inconsistencias en los otros parsers.
Aquí están algunos de los hallazgos más interesantes:
- El problema de "Demasiado Largo": Algunos parsers aceptaban números que eran demasiado grandes para el espacio asignado, o longitudes que no coincidían con los datos. Esto es como un cartero que acepta una carta que dice "Tengo 5 páginas", pero en realidad tiene 100 páginas, causando que el buzón se desborde y colapse.
- La confusión de la "Extensión Desconocida": Cuando un mensaje tenía nuevas funciones que el parser antiguo no conocía, algunos parsers se confundían y empezaban a leer la parte equivocada del mensaje, pensando que era algo completamente distinto. Esto es como un traductor que ve una palabra nueva en un idioma extranjero, se confunde y luego traduce el resto de la oración incorrectamente.
- El error del "Valor por Defecto": Las reglas dicen que si un valor es el "por defecto", no debería enviarse en absoluto para ahorrar espacio. Pero algunos parsers seguían enviándolo, o no reconocían cuando faltaba.
El peligro en el mundo real
El artículo no solo encontró errores teóricos; demostró cómo podrían ser explotados. Los investigadores demostraron cuatro ataques concretos:
- Colapsar un teléfono: Al enviar un mensaje con una lista de IDs de red que era ligeramente demasiado larga (violando una restricción), causaron que el software de un teléfono colapsara, provocando una Denegación de Servicio (DoS).
- Colapsar una torre: Una torre de telefonía comprometida podría enviar un mensaje malformado a otra torre, causando que la segunda torre colapse al intentar procesarlo.
- Filtración de secretos: Si un parser interpreta erróneamente un mensaje debido a una extensión desconocida, podría pensar que una configuración de seguridad está "apagada" cuando en realidad está "encendida", o viceversa. Esto podría llevar a una situación en la que un teléfono cree que se comunica de forma segura, pero la red en realidad está enviando datos en texto plano, permitiendo que los espías lean la información.
- Huella digital de dispositivos (Fingerprinting): Debido a que diferentes parsers manejan los errores de manera distinta, un hacker podría enviar mensajes de "truco" específicos y observar cómo reacciona el dispositivo. Si el dispositivo acepta un mensaje extraño, el hacker sabe que está usando una marca de hardware específica (como una banda base Samsung), lo que le permite atacar ese dispositivo específico con exploits conocidos.
Rendimiento y el Futuro
Los investigadores admiten que su parser perfecto, matemáticamente verificado, no es el más rápido que existe. Es aproximadamente 4 veces más lento que las librerías de C altamente optimizadas que se usan actualmente en la industria. Sin embargo, es 4 veces más rápido que los parsers basados en Python.
El objetivo de VUPER no es reemplazar inmediatamente a los parsers rápidos, sino servir como una implementación de referencia. Así como un maestro chef puede probar un plato y decirte exactamente qué está mal en la receta, VUPER puede decirle a los ingenieros exactamente dónde están fallando sus parsers. Los investigadores esperan que, al usar VUPER para encontrar y arreglar estos errores, la industria pueda eventualmente construir parsers que sean tanto rápidos como matemáticamente garantizados para ser seguros.
Al final, VUPER demuestra que en el complejo y de alta velocidad mundo de 5G y más allá, ya no podemos confiar en un "suficientemente bueno" de pruebas. Necesitamos traductores matemáticamente probados para mantener nuestra ciudad digital segura, protegida y funcionando sin problemas.
¿Ahogado en artículos de tu campo?
Recibe resúmenes diarios de los artículos más novedosos que coincidan con tus palabras clave de investigación — con resúmenes técnicos, en tu idioma.