Progrès révolutionnaire : compilation sécurisée de C vers Rust

2024-12-21

Des chercheurs ont mis au point une nouvelle méthode permettant de compiler du code C en Rust de manière sécurisée. Cette technique utilise l'analyse statique et la traduction dirigée par les types pour éviter de dépendre des blocs `unsafe` de Rust, garantissant ainsi la sécurité mémoire. La méthode a été appliquée avec succès à des codes de la bibliothèque cryptographique HACL* et des bibliothèques EverParse, donnant naissance à une bibliothèque cryptographique moderne vérifiée de 80 000 lignes en Rust pur, une première du genre.