Verificación formal al traducir los crates core y alloc de Rust a Coq

 (formal.land)
1 puntos por GN⁺ 2024-05-16 | 1 comentarios | Compartir por WhatsApp
  • coq-of-rust, que traslada programas en Rust a Coq, empezó a cubrir también los crates core y alloc de la biblioteca estándar, reduciendo la carga de escribir a mano definiciones en Coq para cada función primitive
  • Como estos dos crates son bases de código grandes con mucho código unsafe y Rust avanzado, el reto clave pasó a ser manejar el resultado de la traducción automática en unidades que puedan compilarse y verificarse
  • Al dividir la salida por cada archivo Rust de entrada, alloc quedó en 54 archivos y 171,783 líneas, y core en 190 archivos y 592,065 líneas, lo que facilita la compilación en paralelo y la depuración
  • Los conflictos de nombres de módulos en bloques impl se mitigaron incluyendo información de las cláusulas where, pero los archivos que actualmente no compilan en Coq aún representan el 4% del total
  • El ejemplo de Option::unwrap_or_default muestra un enfoque en el que se prueba la equivalencia entre la definición traducida automáticamente y una definición funcional simple, por lo que se necesitan tanto confianza en la automatización como comprobaciones al momento de la prueba

Tratamiento de primitives de la biblioteca estándar de Rust

  • Formal Land está desarrollando coq-of-rust, que traduce programas en Rust al sistema de demostración formal Coq
  • Antes, para manejar los componentes primitive de la biblioteca estándar de Rust, había que crear por separado una definición en Coq que representara el comportamiento de cada función
  • Para reducir esta carga, se tradujeron los crates core y alloc de Rust con coq-of-rust
  • El resultado de la traducción puede consultarse en las siguientes rutas

Resultados de la primera ejecución de la traducción

  • Al ejecutar coq-of-rust por primera vez sobre alloc y core, se generaron 2 archivos Coq de cientos de miles de líneas correspondientes a cada crate completo
  • Se comprobó que la herramienta podía ejecutarse incluso sobre bases de código grandes, pero el código Coq generado no compilaba de inmediato
  • Los errores aparecían con poca frecuencia, aproximadamente uno cada varios miles de líneas
  • Según cloc, el tamaño del código Rust de entrada era el siguiente
    • alloc: 26,299 líneas de código Rust
    • core: 54,192 líneas de código Rust
  • Como durante el proceso de traducción ocurre expansión de macros, el objetivo real de la traducción es mayor que la cantidad de líneas originales

División del código Coq generado

  • El cambio más grande fue dividir la salida de coq-of-rust en un archivo Coq por cada archivo Rust de entrada
  • Esta división fue posible porque la traducción es insensible al orden de las definiciones y es context-free
  • Entre archivos Rust suele haber dependencias circulares, y Coq no las permite, pero con este enfoque de traducción es posible separar por archivo
  • Después de la división, el tamaño de la salida fue el siguiente
    • alloc: 54 archivos Coq, 171,783 líneas de código Coq
    • core: 190 archivos Coq, 592,065 líneas de código Coq
  • Al dividir los archivos, se hizo más fácil explorar y mantener el código generado
    • Es más sencillo paralelizar la compilación
    • Se puede depurar concentrándose en un archivo a la vez
    • Es más fácil excluir los archivos que no compilan
    • Se vuelve más simple seguir el diff de un solo archivo

Corrección de conflictos de nombres de módulos y archivos restantes

  • Algunos bugs se originaban en conflictos de nombres de módulos de los bloques impl
  • La solución consistió en incluir más información en el nombre del módulo para aumentar su unicidad
    • Se incluyó información de las cláusulas where, que antes faltaba
    • Por ejemplo, en la implementación del trait Default para Mapping<K, V>, el nombre del módulo refleja la condición de que tanto K como V deben implementar Default
  • Actualmente, los archivos que no compilan en Coq son los siguientes
    • alloc/boxed.v
    • core/any.v
    • core/array/mod.v
    • core/cmp/bytewise.v
    • core/error.v
    • core/escape.v
    • core/iter/adapters/flatten.v
    • core/net/ip_addr.v
  • Esto corresponde al 4% del total de archivos
  • Dentro de los archivos que sí compilan todavía hay componentes de Rust no tratados que se axiomatizaron, por lo que no conviene juzgar todo el alcance no soportado solo con este porcentaje

Ejemplo de traducción de Option::unwrap_or_default

  • Option::unwrap_or_default de Rust devuelve x si es Some(x), y llama a T::default() si es None
  • coq-of-rust traduce esto a una definición en Coq en forma monádica
    • Hace match sobre los argumentos de entrada y los tipos
    • En la rama Some, toma el campo de la tupla y lo copia
    • En la rama None, llama al método default del trait core::default::Default
  • En la verificación real se usa una definición funcional más simple en lugar de la definición generada automáticamente
    • Si es None, devuelve core.simulations.default.Default.default
    • Si es Some x, devuelve x
  • La prueba de que la definición generada automáticamente y la definición simple son equivalentes está en CoqOfRust/core/proofs/option.v
  • Si el código Rust original cambia, esa prueba permite detectar el cambio
  • Como la traducción de la biblioteca core se hizo automáticamente, se puede confiar más en la definición generada que en una definición escrita a mano
  • Sin embargo, coq-of-rust también puede tener errores o partes incompletas, por lo que hay que comprobar en el momento de la prueba si el código es válido

Tareas pendientes

  • Aumentó la confianza en la formalización de la biblioteca estándar para la verificación de programas Rust
  • El siguiente objetivo sigue siendo simplificar el proceso de demostración, que aún es tedioso
  • En particular, para demostrar que la simulación es equivalente al código Rust original, se requieren las siguientes tareas
    • Resolución de nombres
    • Introducción de tipos de alto nivel
    • Eliminación de efectos secundarios
  • La dirección de mejora futura es abordar estos pasos por separado

Lecturas relacionadas

1 comentarios

 
GN⁺ 2024-05-16
Opiniones de Hacker News

  • Realmente impresionante.
    Este tipo de traducción automática desplaza el objeto de confianza hacia la herramienta. coq-of-rust en sí no está escrito en Coq sino en Rust, así que la estructura recursiva resulta bastante sorprendente, pero si se mezcla un enfoque al estilo CompCert con la forma de eludir el ataque Trusting Trust de Ken Thompson usando un segundo compilador, como en “Countering Trusting Trust through Diverse Double-Compiling” (2009) de David A. Wheeler [0], parece posible demostrar la corrección.
    Para verificarlo, habría que convertir el traductor coq-of-rust con coq-of-rust de Rust a Coq y, aunque esa traducción se haya hecho con Rust y no se confíe en ella, bastaría con demostrar dentro de Coq las propiedades de corrección deseadas, en particular que al traducir programas Rust a Coq se preserva la semántica.
    Como en el paper, probablemente sea más fácil demostrar usando definiciones más funcionales que las definiciones generadas, así que se puede pasar por un proceso de demostrar equivalencia entre definiciones, como se hace en la biblioteca estándar. Si el traductor coq-of-rust actual, especialmente lib/ [1], tiene 6,350 líneas de Rust, también parece realista escribir todo el traductor en Coq y demostrar que es equivalente al generado.
    Luego, al ejecutar la versión Coq demostrada de coq-of-rust sobre el código fuente en Rust de coq-of-rust, las definiciones Coq resultantes deberían coincidir con la salida del traductor coq-of-rust en Rust usado al principio.
    Como comentario aparte, es bueno ver financiamiento industrial para este tipo de trabajo. Soy bastante cínico con las criptomonedas, pero es cierto que sus requisitos de corrección están impulsando mejoras en áreas que me interesan, como Rust, Coq y el apoyo a estudiantes de maestría que conozco.
    [0]: https://dwheeler.com/trusting-trust/wheelerd-trust.pdf
    [1]: https://github.com/formal-land/coq-of-rust/tree/main/lib

    • Soy uno de los autores, y en efecto un procedimiento así podría ser una buena forma de verificar coq-of-rust.
      Sin embargo, aunque el código en sí sea corto, depende del compilador de Rust para parsear y verificar tipos del código Rust de entrada. Por lo tanto, esa parte también habría que verificarla, o al menos darle una especificación formal sin prueba. El hecho de que la API de rustc sea bastante grande e inestable es un obstáculo, pero aun así podría ser una forma de aumentar la confianza.
    • Me recuerda a cuando trabajaba antes con SPARK Ada. En proyectos sin un target Ada compatible, sobre todo en dispositivos muy pequeños, solíamos convertir Ada a C y luego compilarlo para ese target, lo que permitía hacer varios tipos de análisis estático desde el lado de SPARK.
      Claro que surgía el problema de verificar la salida o el conversor, pero el C resultante era bastante legible para fines de verificación y seguía un estilo limitado, y también había bastante confianza en la herramienta. El análisis estático de SPARK era parte del proceso completo de verificación y validación, y las pruebas y otras actividades aportaban capas adicionales de confianza. En conjunto, fue un enfoque que funcionó bastante bien.
    • La razón por la que las criptomonedas ayudan a este tipo de cosas no es solo por sus restricciones de corrección, sino también porque mucha riqueza pasó a manos de personas interesadas en ciencias de la computación.
      Que gasten ese dinero en investigación en ciencias de la computación no solo les beneficia, también es una forma de filantropía alineada con sus hobbies.
    • No veo bien cómo ese enfoque evita que el compilador de Rust usado para producir binarios inyecte una carga maliciosa. Se podría compilar A con B y B con A y luego comparar los binarios, pero...
      Otro enfoque es el código portador de pruebas. Sería que el compilador de Rust emita junto con el ejecutable una prueba en Coq de que la salida ejecutable coincide con la semántica del código fuente de entrada.
      Claro que también se podría escribir un compilador para un subconjunto de Rust, por ejemplo sin borrow checker ni optimizaciones, hacia código máquina de una arquitectura específica, y desde ahí bootstrapping de todo.

  • El tamaño de los programas verificados de principio a fin con un sistema semiautomático de demostración deductiva como Coq es pequeño. Las bibliotecas pueden ser más fáciles porque el grado de interacción entre el código es menor, pero los programas generales no son así.
    En la práctica, el crecimiento del tamaño de los programas verificables de esta manera ha sido más lento que el crecimiento del tamaño promedio de los programas en general. La verificación de software sólida, es decir, demostrar que coincide al 100% con una especificación, sin duda es útil en lugares como las pruebas de corrección de algoritmos centrales, pero no escala bien.
    Por eso, en parte, la investigación se desplazó hacia métodos no sólidos. El costo de una garantía del 100% puede ser 10 veces el de una garantía del 99.9999%, y esa diferencia de probabilidad puede volverse menor que la probabilidad de fallas ajenas al software. Los sistemas físicos, para empezar, no pueden demostrar que coinciden con una especificación, y también existe la posibilidad de que la propia especificación no coincida lo suficiente con la realidad.

    • El punto clave es que, si se demuestran las partes unsafe de la biblioteca estándar y las garantías de seguridad de Rust, se puede demostrar transitivamente la seguridad de memoria, la ausencia de data races y demás de todo el código Rust seguro que solo use la biblioteca estándar.
      Demostrar que solo el código unsafe es correcto requiere mucho menos esfuerzo que demostrar todo el código Rust. Esto responde a la crítica común de “¿y qué pasa con el código unsafe?” cuando se habla de las garantías de seguridad de Rust. Los huecos que no son lo bastante potentes para cubrirse solo con el sistema de tipos de Rust pueden rellenarse con un sistema más fuerte como Coq.

  • Hay una parte que no entiendo bien en este tipo de intentos. Si hay que convertir el código a Coq de forma manual o semimanual, ¿no es mucho mayor la posibilidad de cometer errores en ese proceso que el beneficio que se obtiene con la verificación formal?
    En otras palabras, ¿cómo sabemos que lo que demostramos sigue siendo válido para el código original?

    • No se puede saber. Al final hay que confiar en algo, ya sea el hardware, el compilador, la especificación, el kernel de confianza de Coq, etc.
      La verificación formal suele discutirse como si eliminara por completo la posibilidad de bugs, pero en la práctica se acerca más a reducirla muchísimo. Aun así, la traducción automática entre Rust y Coq reduce en gran medida la complejidad de aquello en lo que hay que confiar, por lo que debería preferirse frente a una traducción manual
    • Es una limitación real, pero no es una limitación tan mala
      En muchos casos, un bug en la traducción simplemente hace que la demostración sea imposible. Entonces alguien investiga por qué la prueba no pasa y termina encontrando el bug de traducción
      El verdadero problema es cuando un bug de traducción compensa exactamente un bug del código original. Si no hay un riesgo sistemático, es bastante poco probable que dos bugs se anulen entre sí de esa manera
    • El código se traduce automáticamente con coq-of-rust. Si se encuentra un problema en la traducción, basta con corregirlo una vez en la herramienta coq-of-rust, y todos los resultados traducidos se actualizan

  • Para lectores interesados: envié este post porque su contenido relacionado con criptomonedas es menos directo que el de otros posts del mismo blog, pero ahí hay muchos artículos técnicamente más interesantes
    En particular, los dos posts recientes tratan sobre aplicar el mismo enfoque a Python, no a Rust

  • Recuerdo una charla [1] sobre cómo un fuzzer encontró un bug en un compilador de C verificado formalmente. Fue porque la verificación formal no incluía el frontend ni el backend
    Sé que también surge la pregunta de cuánto se puede confiar en Coq en sí o en la traducción, y también me pregunto cómo se sincronizará con las actualizaciones de Rust, pero ni siquiera una verificación formal perfecta significa 100% de corrección de principio a fin
    [1] https://youtu.be/Ux0YnVEaI6A

  • No soy en absoluto experto en verificación formal, pero si la biblioteca base de Rust se verifica formalmente y no usa código unsafe, ¿entonces todos los programas Rust que usen esa biblioteca verificada tendrían, en términos de manejo de memoria, una calidad prácticamente de nivel verificado formalmente?

    • La seguridad de Rust tiene muy poco que ver con los bugs
      Rust tiene su propia definición de “safe”, que puede verse como un subconjunto de la seguridad de memoria. Incluso en código Rust completamente seguro son posibles las carreras de datos, los deadlocks, el agotamiento de memoria y, ni hablar, los errores lógicos
    • Hasta cierto punto creo que ese es el sueño, pero hay muchos matices y varias cosas tienen que encajar
      Primero, hay que formalizar la semántica de unsafe Rust. El trabajo pionero RustBelt[1] de Ralf Jung fue un gran avance, pero aún no está completo. En particular, la procedencia de punteros está resultando ser un elemento complicado
      Segundo, como parte de eso se necesita un modelo formal del borrow checker. Stacked borrows[2] fue un buen intento, pero tiene defectos, y Tree borrows[3] podría corregirlos, aunque también es posible que aparezca algo más sofisticado
      Tercero, se necesita un modelo formal de memoria. Esto trata principalmente del comportamiento de las operaciones atómicas y la sincronización, y por lo tanto es muy importante para componentes de la biblioteca estándar como Arc. Hay amplio consenso en que el modelo de memoria de Rust debe parecerse al de C++ y ser interoperable con él, pero quedan problemas como “out of thin air” y funciones faltantes como seqlock. Esa es una de las razones por las que el kernel de Linux todavía usa su propio modelo
      Cuarto, se necesita una prueba de que las garantías de seguridad se componen bien. En particular, al componer código correcto escrito en unsafe Rust con código safe Rust, las garantías de seguridad deben mantenerse. Hasta ahora hay buenos resultados, pero hay que demostrarlo para todo el sistema
      Quinto, para que esas pruebas sean válidas para todo el código, hay que cerrar todos los bugs de solidez[1] que quedan en Rust. Muchos de estos problemas son teóricos o solo importan realmente en código adversarial[5], así que el progreso es lento
      Incluso después de todo eso, seguiría siendo solo una garantía parcial. Una parte enorme de la superficie de contacto con el sistema se basa en código unsafe. Si solo haces cómputo puro, quizá no, pero si, por ejemplo, construyes una UI gráfica, todavía hay muchísimas cosas que pueden salir mal
      Aun así, hay un camino práctico hacia adelante, y lleva a una situación mucho mejor que el estado común actual de sistemas llenos de vulnerabilidades
      [1]: https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf
      [2]: https://plv.mpi-sws.org/rustbelt/stacked-borrows/
      [3]: https://www.ralfj.de/blog/2023/06/02/tree-borrows.html
      [4]: https://github.com/rust-lang/rust/issues?q=is%3Aissue+is%3Ao...
      [5]: https://github.com/Speykious/cve-rs
    • No soy experto en Rust, pero parece que hay bastante unsafe en el código de core. Tiene sentido que sea así
      https://github.com/search?q=repo%3Arust-lang%2Frust+unsafe+l...
      No creo que Coq, con el enfoque presentado aquí, pueda verificar todas las llamadas unsafe

  • ¿Se puede comparar en qué se diferencia este enfoque de Aeneas o RustHornBelt? ¿Cómo maneja los punteros y los préstamos mutables?

    • No sé cómo funciona RustHornBelt. Nos enfocamos en código seguro, aunque también generamos traducciones de bloques unsafe con un enfoque de “mejor esfuerzo”.
      Comparado con Aeneas, el objetivo es muy parecido, porque ambos buscan verificar programas Rust con un demostrador interactivo de teoremas. Sin embargo, en coq-of-rust escribimos a mano una versión puramente funcional del código que será objeto de la prueba, o la escribimos con ayuda de GitHub Copilot porque es un trabajo repetitivo, y demostramos que es equivalente al resultado de la traducción automática. Aeneas apunta a generar directamente la versión funcional.
      Tratamos todos los punteros como punteros mutables, es decir, como si fueran del tipo *. No usamos la información del borrow checker de Rust; esto simplifica la traducción, pero el costo se paga al momento de la prueba.
      Para razonar sobre punteros en las pruebas, hacemos que el usuario proporcione un asignador personalizado que pueda diseñarse según cómo se vaya a usar la memoria. Por ejemplo, si un programa usa tres variables mutables globales, la memoria puede representarse como un registro con tres campos. Estos campos inicialmente son None para indicar que aún no están asignados.
      Todavía no sabemos qué tan escalable será esta técnica, pero al menos por ahora nos permite evitar el razonamiento con lógica de separación. Esperamos que la mayoría de los programas que queramos verificar, especialmente del lado de aplicaciones, tengan una disciplina de memoria relativamente “simple”.

  • ¿Escribir especificaciones de verificación formal se parece a usar pruebas basadas en propiedades más complejas? Cuando se pasa de programas poco complejos, escribir pruebas basadas en propiedades también se vuelve bastante difícil y consume mucho tiempo.

    • Se parece, pero no siempre es lo mismo. Las pruebas basadas en propiedades normalmente especifican, a nivel de la interfaz del sistema, de funciones o procedimientos, o incluso a un nivel más alto, una descripción de las entradas y prueban si la salida satisface una propiedad o un conjunto de propiedades.
      Al hacer verificación formal en ese mismo nivel, puede verse bastante similar. Pero las herramientas de verificación formal pueden ir más profundo. Por ejemplo, pueden responder preguntas sobre el estado interno del sistema durante un cálculo, como: “tenemos este invariante de bucle, ¿podemos demostrar que realmente se mantiene en todas las iteraciones?” o “¿podemos demostrar que nunca ocurre un underflow/overflow en ningún cálculo intermedio durante esta computación?”.
      Lo primero también podría hacerse con pruebas basadas en propiedades si se extrae el núcleo del bucle a un procedimiento separado y se ejecuta con muchos estados intermedios para probar la propiedad del invariante. Lo segundo es mucho más difícil, a menos que se fragmente el programa de forma extrema hasta que pueda ejecutarse línea por línea por separado.

  • Ni siquiera sabía que algo así fuera posible.
    Me pregunto si este tipo de intentos podría acelerar la adopción de Rust en partes clave de la incorporación al kernel.

  • ¿Alguien podría explicar de forma muy sencilla el concepto de “verificación”? Me intriga por qué existe todo un lenguaje como Coq solo para este propósito, y qué significado práctico tiene para la sociedad en general.