La empresa Amazon y la organización Rust Foundation han presentado una iniciativa destinada a aumentar la seguridad de la biblioteca estándar del lenguaje Rust. El objetivo declarado es verificar la fiabilidad y seguridad de las funciones que utilizan la palabra clave "unsafe", que permite operaciones que trabajan en memoria de manera insegura, como la desreferenciación de punteros, la modificación de variables estáticas y las llamadas a bibliotecas externas en C/C++. Se informa que actualmente la biblioteca estándar de Rust cuenta con aproximadamente 35,000 funciones, de las cuales en 7,500 se encuentran bloques de código que se ejecutan en un contexto "unsafe". En los últimos tres años, se han identificado 57 problemas de corrección en la biblioteca, de los cuales 20 han sido etiquetados como vulnerabilidades.
El trabajo para verificar la biblioteca se organiza en forma de concurso, en el que se proponen diversas tareas relacionadas con la realización de verificaciones específicas para confirmar el trabajo seguro con la memoria de las bibliotecas Rust o con el desarrollo de herramientas para automatizar dichas verificaciones. La realización exitosa del objetivo de verificación (proporcionar una prueba formal de fiabilidad) implica el pago de una recompensa. Se ha creado un repositorio para realizar experimentos y publicar los resultados, que es una bifurcación del repositorio oficial de Rust.
Actualmente se han propuesto 13 tareas. Por ejemplo, en una de las tareas se solicita comprobar la seguridad del trabajo con punteros raw en las funciones del módulo core::ptr y proporcionar una prueba formal de la corrección de las operaciones con punteros. Para la verificación, se pueden utilizar herramientas existentes, como Aeneas, Kani, Gillian, Verus y Creusot, o proponer nuevas. Ejemplos de tareas completadas.
Fuente: opennet.ru
