Simple Science

Ciencia de vanguardia explicada de forma sencilla

# Informática# Ingeniería del software

El marco de IA 3DGen transforma el análisis de datos

3DGen usa IA para convertir descripciones de datos informales en código seguro.

― 9 minilectura


IA en el análisis deIA en el análisis dedatosde manera segura y efectiva.La IA ayuda en la generación de código
Tabla de contenidos

Parsear datos es una parte clave de muchos sistemas de software. Se trata de tomar información en un formato y convertirla en una estructura útil que una computadora pueda manejar. Pero cuando el parseo viene de fuentes que no están definidas estrictamente, como documentos en lenguaje natural, pueden surgir problemas. Si un programa de computadora no entiende correctamente la entrada, puede llevar a agujeros de seguridad que los atacantes podrían explotar. Muchos desarrolladores a menudo tienen que traducir descripciones informales de formatos de datos a Código preciso, y eso puede ser complicado, especialmente al usar lenguajes que no son seguros en cuanto a la memoria.

En el pasado, los investigadores han intentado crear lenguajes formales que ayuden a definir formatos de datos. Estos lenguajes formales se pueden usar para generar código que sea eficiente y seguro. Pero crear reglas formales a partir de descripciones informales no es fácil. Aquí es donde entra un nuevo marco, 3DGen. Este marco usa IA para ayudar a convertir información informal mixta, como documentos en lenguaje natural, en Especificaciones claras. Trabaja con un lenguaje específico llamado 3D.

3DGen no solo crea una especificación; también ayuda a verificar que las especificaciones sean precisas, produciendo Pruebas que pueden validarlas. Este enfoque dual asegura que el código final que se genera sea seguro y correcto.

El Problema con el Parseo Informal

Cuando el software parsea datos, especialmente cuando provienen de un atacante, pueden haber serios riesgos involucrados. Muchas vulnerabilidades en el software surgen de un parseo incorrecto de esos datos. Los desarrolladores a menudo se refieren a documentos que describen formatos de datos, pero pueden no interpretar estos formatos informales correctamente. Esto puede pasar cuando los programadores pasan de leer documentos a escribir código en lenguajes de programación de bajo nivel, que son conocidos por ser menos seguros en términos de gestión de memoria.

Por ejemplo, la estructura de los encabezados TCP, que son esenciales en las comunicaciones de red, se describe en lenguaje natural en ciertos documentos llamados RFCs (Request for Comments). Un pequeño error en el parseo de esos formatos puede permitir que alguien explote el software. De hecho, incluso un sistema muy utilizado como el núcleo de Linux tuvo que ser parcheado después de 20 años de usar un parser de encabezados TCP incorrecto.

Para abordar estos problemas, los investigadores han creado lenguajes diseñados específicamente para definir formatos binarios. Estos lenguajes vienen con herramientas que generan código para manejar el parseo y la serialización de datos de manera segura. Una de esas herramientas es EverParse, que crea código verificado a partir de una descripción hecha en un lenguaje de parseo único.

Los Desafíos de la Especificación Formal

En un escenario perfecto, las especificaciones para formatos de datos siempre se escribirían usando lenguajes precisos que pudieran generar código ejecutable confiable. Sin embargo, la mayoría de las veces, estas especificaciones se escriben en estilos informales. Pueden provenir de una mezcla de documentos en lenguaje natural, código de ejemplo y pares de entrada/salida. Traducir este tipo de documentos en especificaciones formales es una tarea laboriosa y a menudo compleja.

El proceso generalmente se ve así:

  1. Aprender un nuevo lenguaje diseñado para tareas específicas.
  2. Entender cómo la especificación informal articula la estructura de parseo deseada.
  3. Escribir este entendimiento en el lenguaje formal.
  4. Revisar y refinar los pasos anteriores según sea necesario.

Dado estos desafíos, los desarrolladores a menudo omiten escribir especificaciones formales por completo y se van directo a codificar. Esto puede llevar a errores que podrían abrir vulnerabilidades en el software.

Introduciendo 3DGen

3DGen es un nuevo marco que tiene como objetivo reducir el esfuerzo involucrado en traducir especificaciones informales a código ejecutable. Utiliza efectivamente agentes de IA para ayudar a convertir descripciones informales en especificaciones utilizando un lenguaje específico llamado 3D. El objetivo principal de 3DGen es ayudar a los programadores a crear parsers de formatos de datos seguros y eficientes.

El marco opera centrado en un ciclo de refinamiento de la intención del usuario. Ayuda a los usuarios a definir una especificación que coincida con el comportamiento de un modelo conocido y correcto, al que podemos referirnos como un oráculo. Dentro de este proceso, 3DGen también emplea una técnica para generar automáticamente pruebas que validen el código generado contra el comportamiento del oráculo.

Al refinar las especificaciones de manera iterativa y validarlas a través de pruebas, 3DGen produce una especificación confiable que finalmente lleva a un código seguro y correcto en C.

Flujo de Trabajo de 3DGen

El flujo de trabajo principal de 3DGen es el siguiente:

  1. Aprender el Lenguaje: El lenguaje 3D es simple y se basa en una sintaxis comúnmente conocida de C, como typedefs y estructuras. El manual de 3D es conciso, lo que facilita que los agentes de IA aprendan a generar código basado en este lenguaje.

  2. Recopilar Información: Los usuarios recopilan todas las especificaciones informales relevantes, que pueden incluir documentos, ejemplos y otros formatos de entrada. Esta información recopilada se presenta al marco.

  3. Generar Especificaciones: Usando los datos recopilados, los agentes de IA generan especificaciones candidatas en formato 3D.

  4. Refinar Especificaciones: Las especificaciones generadas se revisan para detectar errores, y cualquier error identificado es corregido por los agentes. También generan casos de prueba adicionales para asegurarse de que las especificaciones cumplan con el comportamiento esperado.

  5. Generar Código Verificado: Una vez que se logra una especificación satisfactoria, el marco genera código C verificado que puede parsear de manera segura los mensajes formateados según las especificaciones.

Evaluación de 3DGen

3DGen ha sido probado en una variedad de formatos de datos estándar utilizados en Internet. La evaluación mostró que fue capaz de producir especificaciones confiables que conducen a un código C correcto a gran escala. El uso de un lenguaje específico para el parseo ayuda a agilizar el proceso, facilitando al AI generar el código necesario.

En aplicaciones del mundo real, donde existen muchos protocolos, 3DGen ha demostrado su capacidad para construir estas especificaciones mientras verifica su precisión a través de pruebas automatizadas. Esta habilidad brinda un nuevo nivel de confianza de que el código generado no solo funciona, sino que también es seguro y apropiado para su uso en software que depende de dichas especificaciones.

Desafíos Enfrentados por los Agentes de IA

Aunque 3DGen puede ayudar a generar especificaciones con precisión, los agentes de IA dentro del marco aún enfrentan desafíos. A menudo deben refinar su comprensión de la información que se les presenta. Pueden ocurrir errores cuando el lenguaje informal es ambiguo o cuando malinterpretan el significado detrás de las especificaciones.

Por ejemplo, si la documentación de especificación no transmite claramente el orden de los valores o restricciones específicas, los agentes pueden generar código incorrecto. Además, aunque pueden aprender de errores previos, errores de sintaxis iniciales pueden ralentizar el proceso.

A pesar de estos problemas, los agentes pueden producir código válido después de varias iteraciones refinando su salida a través de comentarios de las pruebas.

La Importancia de los Casos de Prueba

El proceso de prueba es crítico para asegurar que el código generado cumpla con los requisitos establecidos en las especificaciones originales. 3DGen emplea una técnica de generación de pruebas que crea varios casos de prueba para evaluar el comportamiento del código en comparación con los resultados esperados. Esto ayuda a identificar errores temprano en el proceso de desarrollo, permitiendo mejoras inmediatas.

Los agentes de IA utilizan una mezcla de capturas de paquetes del mundo real y casos generados sintéticamente para construir una suite de pruebas diversa. Al probar en una amplia gama de escenarios, el marco puede confirmar la solidez de las especificaciones generadas y la corrección del código resultante.

Comparando Especificaciones Generadas con las Manuscritas

Además de evaluar las capacidades de 3DGen, las comparaciones con especificaciones manuscritas brindan información valiosa. Se midieron las fortalezas y debilidades de las especificaciones generadas por IA frente a las creadas por desarrolladores experimentados. A través de pruebas diferenciales, se encontró que, si bien hubo instancias en las que las especificaciones generadas por IA eran equivalentes a las manuscritas, también hubo casos donde revelaron restricciones faltantes en las versiones manuscritas.

Esto sirve como recordatorio de que incluso las especificaciones escritas por expertos pueden albergar errores, y usar herramientas de IA como 3DGen puede ayudar a descubrir y abordar estos problemas.

Conclusión

El viaje desde especificaciones informales a código funcional está lleno de desafíos. Los errores en el parseo pueden llevar a vulnerabilidades significativas, y el proceso manual de traducir especificaciones puede ser engorroso. Sin embargo, marcos como 3DGen demuestran cómo la IA puede ayudar a crear y verificar especificaciones de manera efectiva.

Al aprovechar el poder de la IA, 3DGen no solo ayuda a los desarrolladores a escribir código más preciso y seguro, sino que también abre la puerta para que no expertos se involucren más fácilmente con lenguajes específicos del dominio. A medida que la tecnología de IA continúa avanzando, el potencial de crear sistemas de software confiables que puedan manejar formatos de datos complejos de manera segura se vuelve más alcanzable.

De cara al futuro, 3DGen y marcos similares jugarán un papel esencial en el desarrollo de sistemas de parseo seguros y confiables, destacando la importancia de combinar la tecnología con la supervisión humana en el proceso de programación.

En resumen, la aplicación de IA en la especificación formal y la generación de código ofrece ventajas significativas para el desarrollo de software, particularmente cuando se trata de manejar formatos de datos de fuentes informales. El continuo refinamiento de estas herramientas ofrece un camino prometedor hacia sistemas de software más robustos y seguros.

Fuente original

Título: 3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers

Resumen: Improper parsing of attacker-controlled input is a leading source of software security vulnerabilities, especially when programmers transcribe informal format descriptions in RFCs into efficient parsing logic in low-level, memory unsafe languages. Several researchers have proposed formal specification languages for data formats from which efficient code can be extracted. However, distilling informal requirements into formal specifications is challenging and, despite their benefits, new, formal languages are hard for people to learn and use. In this work, we present 3DGen, a framework that makes use of AI agents to transform mixed informal input, including natural language documents (i.e., RFCs) and example inputs into format specifications in a language called 3D. To support humans in understanding and trusting the generated specifications, 3DGen uses symbolic methods to also synthesize test inputs that can be validated against an external oracle. Symbolic test generation also helps in distinguishing multiple plausible solutions. Through a process of repeated refinement, 3DGen produces a 3D specification that conforms to a test suite, and which yields safe, efficient, provably correct, parsing code in C. We have evaluated 3DGen on 20 Internet standard formats, demonstrating the potential for AI-agents to produce formally verified C code at a non-trivial scale. A key enabler is the use of a domain-specific language to limit AI outputs to a class for which automated, symbolic analysis is tractable.

Autores: Sarah Fakhoury, Markus Kuppe, Shuvendu K. Lahiri, Tahina Ramananandro, Nikhil Swamy

Última actualización: 2024-05-06 00:00:00

Idioma: English

Fuente URL: https://arxiv.org/abs/2404.10362

Fuente PDF: https://arxiv.org/pdf/2404.10362

Licencia: https://creativecommons.org/licenses/by/4.0/

Cambios: Este resumen se ha elaborado con la ayuda de AI y puede contener imprecisiones. Para obtener información precisa, consulte los documentos originales enlazados aquí.

Gracias a arxiv por el uso de su interoperabilidad de acceso abierto.

Más de autores

Artículos similares