La tecnología de traducción automática de C a Rust proporciona una precisión que va más allá de la IA

Dado que el lenguaje C, que forma la base de software global crítico como los sistemas operativos, enfrenta limitaciones de seguridad, el equipo de investigación de KAIST es pionero en la investigación de tecnología original central para la conversión automática precisa a Rust para reemplazarlo. Al demostrar la corrección matemática de la conversión, una limitación de los métodos de inteligencia artificial (LLM) existentes y resolver los problemas de seguridad del lenguaje C mediante la conversión automática a Rust, presentaron una nueva dirección y visión para la futura investigación de seguridad del software.

El artículo del equipo de investigación del profesor Sukyoung Ryu de la Escuela de Computación fue publicado en la edición de noviembre de Comunicaciones de la ACM y fue seleccionado como artículo de portada.

El lenguaje C se ha utilizado ampliamente en la industria desde la década de 1970, pero sus limitaciones estructurales han causado continuamente graves errores y vulnerabilidades de seguridad. Rust, por su parte, es un lenguaje de programación seguro desarrollado desde 2015, utilizado en el desarrollo de sistemas operativos y navegadores web, y tiene la característica de poder detectar y prevenir errores antes de la ejecución del programa.

La Casa Blanca de EE. UU. recomendó suspender el uso del lenguaje C en un informe tecnológico publicado en febrero de 2024, y la Agencia de Proyectos de Investigación Avanzada de Defensa (DARPA) también declaró explícitamente que Rust es la alternativa principal para resolver los problemas de seguridad del lenguaje C al promover un proyecto para desarrollar tecnología para la conversión automática de código C a Rust.

El equipo de investigación del profesor Ryu planteó de manera proactiva las cuestiones de la seguridad del lenguaje C y la importancia de la conversión automática incluso antes de que estos movimientos comenzaran en serio, y han desarrollado continuamente tecnologías centrales relacionadas.

En mayo de 2023, el equipo de investigación presentó la tecnología de conversión Mutex (necesaria para la sincronización de programas) en ICSE (Conferencia Internacional sobre Ingeniería de Software). En junio de 2024, presentaron la tecnología de conversión de parámetros de salida (utilizada para la entrega de resultados) en PLDI (Diseño e implementación de lenguajes de programación), y en octubre del mismo año, presentaron la tecnología de conversión Union (para almacenar diversos datos juntos) en ASE (Automated Software Eng).

El Dr. Jaemin Hong afirmó: «La tecnología de conversión que desarrollamos es una tecnología original basada en la teoría del lenguaje de programación, y su mayor fortaleza es que podemos demostrar lógicamente la ‘corrección’ de la conversión». Y añadió: «Si bien la mayoría de las investigaciones se basan en modelos de lenguaje grandes (LLM), nuestra tecnología puede garantizar matemáticamente la corrección de la conversión».

Está previsto que el Dr. Hong sea nombrado profesor asistente en el Departamento de Ciencias de la Computación de la UNIST a partir de marzo de 2025.

Además, el equipo de investigación del profesor Ryu tiene cuatro artículos, incluida la tecnología de conversión C→Rust, aceptados para su presentación en ASE 2025 celebrada en Seúl, Corea del Sur, del 16 al 20 de noviembre.

Estos artículos, además de la tecnología de conversión automática, cubren varios campos de ingeniería de software de vanguardia. Incluyen: tecnología para verificar si los programas informáticos cuánticos funcionan correctamente, tecnología «WEST» que verifica automáticamente la corrección de los programas WebAssembly (tecnología para la ejecución rápida y eficiente de programas en la web) y crea pruebas para ellos, y tecnología que simplifica automáticamente el código complejo de WebAssembly para encontrar errores rápidamente. Entre ellos, el artículo de WEST recibió el premio al artículo distinguido.