Un método formalizado para compilar C a Rust seguro

 (arxiv.org)
2 puntos por GN⁺ 2024-12-22 | 1 comentarios | Compartir por WhatsApp

  • Compilar C a Rust seguro

  • El lenguaje Rust ha ganado popularidad rápidamente, pero muchas bases de código importantes siguen estando escritas en C y reescribirlas manualmente no resulta realista. Por ello, traducir C a Rust de forma automática surge como una alternativa atractiva.

  • Múltiples investigaciones existentes avanzan hacia procesar cada vez más partes de C utilizando diversas características de Rust (por ejemplo, unsafe). Sin embargo, aunque la automatización es atractiva, generar código que depende de unsafe invalida las garantías de seguridad de memoria que Rust proporciona, y por tanto se pierde el beneficio principal de portar una base de código existente a un lenguaje seguro en memoria.

  • Exploramos una ruta alternativa para traducir C a Rust seguro: generar código conforme con el sistema de tipos de Rust, de modo que la seguridad de memoria se garantice fácilmente.

  • Nuestra investigación incluye varias contribuciones novedosas:

    • Traducción dirigida por tipos de partes de C a Rust seguro
    • Un nuevo análisis estático basado en árboles de segmentos que permite expresar la aritmética de punteros de C usando slices y operaciones de partición de Rust
    • Un análisis para inferir con precisión qué préstamos deben ser mutables
    • Una estrategia de compilación compatible con tipos de estructuras de C para la distinción de asignación sin propiedad y con propiedad de Rust

  • Aplicamos esta metodología a una base de código de C ya verificada formalmente: la biblioteca de criptografía HACL* y los analizadores y serializadores binarios de EverParse. Mostramos que el subconjunto de C compatible es suficiente para traducir ambas aplicaciones a Rust seguro.

  • En la evaluación, observamos que para algunas partes que violan la disciplina de aliasing de Rust basta una reescritura quirúrgica automatizada, y que el impacto en el rendimiento de algunas copias estratégicas insertadas es mínimo.

  • En particular, al aplicar el enfoque a HACL*, obtuvimos que una biblioteca criptográfica verificada de 80.000 líneas que implementa todos los algoritmos modernos esté escrita enteramente en Rust. Este es el primer caso.

Lecturas relacionadas

1 comentarios

 
GN⁺ 2024-12-22
Comentario de Hacker News

  • Al portar un proyecto a Rust, saqué algunas conclusiones

    • Convertir un programa en C a Rust permite encontrar bugs más rápido gracias a las restricciones estrictas de Rust
    • La conversión automática de C a Rust no está completamente resuelta porque ambos lenguajes tienen diseños fundamentalmente distintos
    • En algunos casos, portear de C a Rust puede ser imposible, debido a la inseguiridad intrínseca del propio diseño
    • El avance de las herramientas hará que el proceso de porteo sea más fluido

  • Las bases de código de C formalmente verificadas y las bases de código de sistemas C comunes no son lo mismo

  • En 2002, investigadores publicaron un paper sobre Cyclone, un dialecto seguro de C, y al portar código de C a Cyclone encontraron bugs de seguridad

    • Este tipo de traducciones manuales o automáticas puede aumentar la adopción de lenguajes seguros y descubrir bugs existentes

  • Una traducción simple a Rust puede generar partes seguras y partes inseguras, y el trabajo manual puede centrarse en verificar la seguridad de las zonas inseguras

    • Puede haber ventajas incluso si la parte insegura es grande

  • Tengo pocas expectativas de que un enfoque de compilar solo una parte pequeña de C funcione bien

    • Porque el modelo de ownership de Rust se diferencia demasiado del de un programa real en C

  • Curiosidad sobre cómo comparar con la conversión de C en Zig

    • Zig genera bien un entorno mixto con código nuevo y código C existente, y también puede usarse como compilador de C
    • Tengo curiosidad sobre por qué los mantenedores del kernel de Linux no lo consideran como alternativa a C

  • Pregunta de si C2Rust puede generar código formalmente correcto

    • No se ve un enlace al código fuente desde el que se genera el código Rust

  • Si una librería de C ya funciona, puede valer la pena migrar usando la inseguridad de Rust

    • Rust generalmente carece de librerías

  • Es interesante que niveles altos de optimización no mejoran demasiado la velocidad de Rust

    • Tengo curiosidad sobre qué tan bien funcionaría compilar C a Rust de una sola vez con optimización O3