Tecnología de verificación de Rust aplicada a código de sistemas de bajo nivel

 (github.com/verus-lang)
1 puntos por GN⁺ 2024-05-06 | 1 comentarios | Compartir por WhatsApp
  • Verus es una herramienta para verificar la corrección de código escrito en Rust; cuando el desarrollador especifica lo que el código debe hacer, comprueba estáticamente si el código Rust ejecutable satisface esa especificación en todas las ejecuciones posibles
  • En lugar de agregar verificaciones en tiempo de ejecución, usa solvers potentes para demostrar que el código es correcto, y actualmente solo admite una parte de Rust
  • En algunos casos, puede comprobar estáticamente incluso la corrección de código que manipula raw pointers, más allá del sistema de tipos estándar de Rust
  • El proyecto está en desarrollo activo y puede tener funciones rotas o faltantes, y la documentación aún no está completa, por lo que los usuarios deben estar preparados para pedir ayuda en Zulip
  • Como rutas para aprender y experimentar, ofrece Verus Playground en el navegador, guía de instalación, tutorial y referencia, documentación de la API de la biblioteca estándar, guía para verificar código concurrente, además de ejemplos y pruebas

Qué verifica Verus

  • Verus es una herramienta para verificar la corrección de código Rust
  • El desarrollador escribe como especificación el comportamiento que el código debe cumplir
  • Verus comprueba estáticamente que el código Rust ejecutable satisfaga siempre esa especificación en todas las ejecuciones posibles
  • En vez de añadir verificaciones en tiempo de ejecución, usa solvers para demostrar que el código es correcto
  • Actualmente el alcance de soporte es un subconjunto de Rust, y se está trabajando para ampliarlo
  • En algunos casos, puede verificar estáticamente, más allá del sistema de tipos estándar de Rust, la corrección de código que por ejemplo manipula raw pointers

Estado de desarrollo y precauciones de uso

  • Verus es un proyecto en desarrollo activo
  • Algunas funciones pueden estar rotas o ausentes
  • La documentación todavía no está completa
  • Si quieres probar Verus, necesitas estar preparado para pedir ayuda en Zulip
  • La comunidad de Verus ha publicado varios artículos de investigación, y distintos proyectos de la industria y la academia usan Verus
  • La lista relacionada puede consultarse en la página de publications and projects

Cómo empezar y herramientas de desarrollo

  • Para probar Verus en el navegador, puedes usar Verus Playground
  • Para un desarrollo más formal, debes seguir la guía de instalación
  • El aprendizaje puede comenzar en Tutorial and reference
  • También admite el formateador automático verusfmt para código Verus

Documentación y materiales de aprendizaje

Ejemplos y participación en la comunidad

  • Los ejemplos de uso de Verus ofrecen varios puntos de partida además de la documentación
    • Publications and projects: publicaciones y proyectos que usan Verus
    • Videos, slides, and exercises: videos, diapositivas y ejercicios de un tutorial de Verus de un día
    • Standalone examples: ejemplos independientes que usan Verus en tareas pequeñas y concretas
    • Small and medium-sized examples: ejemplos que muestran varias funciones de Verus
    • Unit tests: pruebas con ejemplos de sintaxis y funciones de Verus
  • Los reportes de issues y las discusiones pueden realizarse en GitHub o en Zulip
  • Para solicitudes de funciones y conversaciones abiertas se usa GitHub discussions, mientras que los bugs reproducibles de funciones existentes se registran en GitHub issues
  • Si quieres contribuir con código, puedes consultar la guía de Contributing to Verus

Lecturas relacionadas

1 comentarios

 
GN⁺ 2024-05-06
Comentarios de Hacker News

  • Probé escribir un controlador de Kubernetes verificado formalmente con Verus
    En esencia, se pueden demostrar propiedades de vivacidad como “eventualmente el controlador ajusta el clúster al estado objetivo solicitado”
    Aun así, cuando el estado objetivo cambia rápido, y considerando asincronía, fallos, etc., incluso especificar qué significa “correctitud” tiene bastantes sutilezas
    Código: https://github.com/vmware-research/verifiable-controllers/, y el artículo relacionado aparecerá en OSDI 2024

    • Me pregunto qué aporta por encima de las pruebas unitarias

  • Como un pequeño paso intermedio hacia Verus, se puede usar debug_assert de Rust para precondiciones y poscondiciones
    El compilador de Rust normalmente las elimina en builds de producción
    Los ejemplos de verificación del tutorial de Verus escriben rangos de entrada y condiciones del resultado con requires y ensures, y la versión con comprobaciones en tiempo de ejecución verifica esas mismas condiciones durante la ejecución, por ejemplo debug_assert(-16 <= x1) y debug_assert(x8 == 8 * x1)

    • Un problema actual de la sintaxis de Verus es que hay que envolver todo el código en un macro procedural
      Otras herramientas de Rust para prueba/verificación/diseño por contratos, como Creusot, usan sintaxis basada en atributos, que en general se siente más liviana y más idiomática de Rust
      Estaría bien que una futura versión de Verus también permitiera algo así
    • Ojalá más gente usara este tipo de assert
      Es excelente como herramienta de documentación y complementa muy bien al sistema de tipos y a las pruebas
    • También se puede probar el crate "contracts": https://docs.rs/contracts/latest/contracts/
    • Los ejemplos de Verus se parecen a cómo escribo código en Clojure
      A la mayoría de las funciones les pongo precondiciones y poscondiciones, y en la JVM hay una bandera para quitarlas fácilmente en builds de producción

  • Pregunto desde alguien sin mucha experiencia real en ciencias de la computación: en el README, cuando dice “verificar la correctitud del código”, ¿qué diferencia hay entre verificación y eso de “prueba” que mencionan en otros lados?
    También me interesan recursos para que un programador profesional sin una base fuerte en ciencias de la computación/matemáticas aprenda a “probar” cosas sobre código
    Además, no termino de entender por qué las pruebas de conocimiento cero son tan importantes o relevantes. Por ejemplo, he escuchado cosas como x.com/ZorpZK, pero no entiendo por qué sería tan genial

    • Software Foundations es un buen recurso para aprender verificación de código junto con programación funcional: https://softwarefoundations.cis.upenn.edu
      Eso sí, Verus y Coq, que es lo que usa Software Foundations, siguen enfoques distintos
      Verus intenta demostrar propiedades automáticamente con un resolvedor SMT, un sistema automático de resolución de restricciones, mientras que Coq exige demostrar muchas más cosas manualmente y tiene automatización limitada
      Ambos tienen ventajas y desventajas; la automatización es genial cuando funciona, pero frustrante cuando no
      Las pruebas de conocimiento cero son más bien otro campo; mucha gente que trabaja en verificación/pruebas formales ni siquiera las toca. Es mejor pensarlas como un primitivo criptográfico
    • Aquí están usando verificación y prueba como sinónimos, y eso también queda claro más adelante en el primer párrafo
      Las pruebas de conocimiento cero tienen bastante sobrecarga y todavía les falta una supuesta “killer app”, así que su utilidad práctica, importancia o relevancia todavía no es tan grande, aunque conceptualmente son interesantes
    • En este contexto, “verificación” y “prueba” son lo mismo
      Ojalá yo también tuviera buenos materiales de aprendizaje. La documentación de Dafny es bastante buena, pero la verificación formal de software todavía no parece estar en un punto en que programadores comunes, sin doctorado en ciencias de la computación o matemáticas, puedan usarla fácilmente
      Viendo los ejemplos parece relativamente fácil, pero enseguida te topas con “no se puede demostrar”, y la explicación del porqué suele meterse en detalles de implementación tan profundos que probablemente solo quien lo escribió los entiende
    • Hasta donde sé, una prueba de conocimiento cero te permite demostrar que sabes algo sin revelar ese algo
      Por ejemplo, podrías verificar que conoces una contraseña sin enviársela al servidor, haciendo más difícil que un servidor malicioso o un atacante en el medio la robe
      También podría ofrecer mejores opciones para verificar identidad. Podrías demostrar que tienes una identificación oficial sin entregar el documento al servidor, lo que reduce casos de “guardarlo por hasta 2 años / 3 años / 6 meses” para que al final igual se filtre
    • Me parece que hablar de “un programador profesional que demuestra cosas sobre código” sigue siendo casi una contradicción
      Hacer pruebas sobre código todavía no es algo que hagan los programadores profesionales
      La lógica de Hoare es un buen punto de partida, y a veces incluso se enseña en cursos introductorios de ciencias de la computación
      Coq tiene una curva de aprendizaje pronunciada, y es todavía más difícil si no estás familiarizado con OCaml o un lenguaje parecido. Why3 quizá sea más amigable para principiantes: https://www.why3.org
      Prueba y verificación pueden significar lo mismo, pero “prueba” suena más interactivo, mientras que “verificación” da la idea de algo que puede automatizarse, como model checking o resolver SMT sobre programas anotados

  • Para quien no conozca proyectos parecidos, Dafny es un “lenguaje de programación con conciencia de verificación” que puede compilar a Rust: https://github.com/dafny-lang/dafny

  • Se ve realmente genial. Sería útil para la gente tener una guía o ejemplos de cómo agregar pruebas a una base de código existente
    Por ejemplo, supongamos una app GUI mínima con solo un cuadro de texto que recibe por HTTP un arreglo no confiable que no puede conocerse en tiempo de compilación, lo ordena con bubble sort y luego lo muestra
    El bubble sort tiene un bug intencional de off-by-one por el cual el último elemento queda sin ordenar, y las pruebas unitarias por casualidad no detectan ese bug. La preocupación de que las pruebas sean incompletas podría ser una motivación principal para pasar a pruebas formales
    Luego estaría bueno mostrar cómo se reemplazan las pruebas unitarias por pruebas formales, descubriendo y corrigiendo el bug en el proceso
    No hace falta explicar en detalle el código de prueba en sí; bastaría con enfocarse en detalles prácticos como el límite entre el código matemático probado y el código de E/S no probado, la línea de comandos usada para probar y compilar, y algo como un archivo zip que uno pueda tocar directamente
    De hecho, probablemente con solo leer de stdin y escribir a stdout sería suficiente

  • Uno de los principales contribuidores dio una excelente charla sobre Verus en el meetup de Rust de Zürich: https://www.youtube.com/watch?v=ZZTk-zS4ZCY
    Me impresionó lo limpiamente que encaja este código “ghost” dentro del programa, y me recordó un poco a Ada

  • Me pregunto si Rust también tiene ya un estándar, como C/C++, Common Lisp o Ada/SPARK2014
    Si no lo tiene, eso lo vuelve un blanco móvil en comparación con las herramientas de verificación desarrolladas para Ada/SPARK2014
    Tampoco es fácil ignorar la herencia de Ada/SPARK2014, que va desde bare metal hasta aplicaciones críticas de seguridad de alta integridad

  • Me pregunto qué relación hay entre esto y Kani. ¿Funcionan de manera distinta?
    https://github.com/model-checking/kani

    • Los model checkers suelen explorar solo una cantidad limitada de estados, así que son eficientes para encontrar bugs y muchas veces no requieren anotaciones adicionales en el programa
      Los verificadores automáticos basados en SMT, como Verus, Dafny, F* y mi propio VCC, requieren anotaciones en casi todas las funciones y bucles, pero ofrecen garantías más amplias sobre la corrección del programa
      Las herramientas basadas en asistentes de prueba interactivos como Coq o Lean normalmente requieren todavía más guía del usuario, pero pueden garantizar propiedades más complejas

  • Me pregunto cómo se compara Verus con SPARK
    ¿Es un verificador de la misma categoría general? Más allá de que sea un verificador para Rust en vez de uno para Ada, ¿en qué se diferencia Verus?

  • Sería bueno que alguien que conozca bien Verus pudiera explicar la diferencia en rendimiento y expresividad entre Verus y Lean4
    Entiendo que Verus es una herramienta de verificación basada en SMT, mientras que Lean es un asistente de prueba interactivo y también una herramienta basada en SMT
    Pero mi entendimiento del campo de la verificación formal es limitado, así que me interesa la opinión de alguien que conozca bien los métodos formales de software

    • Lean es parecido a Coq
      Por ejemplo, se pueden plantear y demostrar proposiciones sobre código C, como en el libro “Software Foundations” de Coq, pero parece que casi nadie lo hace con Lean y faltan herramientas
      También se puede escribir un programa en Lean4 y demostrar propiedades sobre ese programa, y hay algunas personas haciéndolo poco a poco
      Formalizar matemática pura y publicar artículos sobre eso es actualmente el uso principal de Lean4 y Coq
      Los tipos de cosas que Lean/Coq realmente pueden expresar y demostrar son más generales, pero puede que esa generalidad no sea necesaria para programas del mundo real