Une méthode formalisée pour compiler du C en Rust sûr

 (arxiv.org)
2 points par GN⁺ 2024-12-22 | 1 commentaires | Partager sur WhatsApp

  • Compiler du C en Rust sûr

  • La popularité du langage Rust connaît une forte hausse, mais de nombreux codebases importants sont encore écrits en C, et les réécrire manuellement n’est pas réaliste. Par conséquent, la traduction automatique du C vers le Rust s’impose comme une alternative attrayante.

  • Plusieurs travaux existants cherchent à traiter une part de plus en plus grande du C en utilisant diverses fonctionnalités de Rust (par exemple unsafe). Bien que l’automatisation soit prometteuse, générer du code dépendant de unsafe invalide les garanties de sécurité mémoire offertes par Rust, et l’avantage principal d’un portage d’une base de code existante vers un langage à sécurité mémoire disparaît.

  • Nous explorons une autre voie pour traduire le C vers du Rust sûr : générer du code qui respecte le système de types de Rust afin de garantir facilement la sûreté mémoire.

  • Notre recherche apporte plusieurs contributions originales :

    • Une traduction orientée types d’une partie du C vers du Rust sûr
    • Une nouvelle analyse statique basée sur des «split trees» pour exprimer l’arithmétique des pointeurs C via les slices et les opérations de découpage de Rust
    • Une analyse qui infère exactement quels emprunts doivent être mutables
    • Une stratégie de compilation pour les types de structures C compatibles avec la distinction de Rust entre allocations possédées et non possédées

  • Nous avons appliqué cette approche à des bases de code C formellement vérifiées existantes : la bibliothèque cryptographique HACL* et le parseur binaire ainsi que le sérialiseur d’EverParse. Nous montrons que le sous-ensemble de C pris en charge suffit à traduire ces deux applications en Rust sûr.

  • Les résultats de l’évaluation montrent que, pour certaines parties qui violent la discipline d’aliasing de Rust, une réécriture chirurgicale automatisée suffit et que l’impact sur les performance des copies stratégiques insérées est minime.

  • En particulier, l’application de cette approche à HACL* a abouti à une bibliothèque cryptographique vérifiée de 80 000 lignes implémentant tous les algorithmes modernes, entièrement écrite en Rust pur. C’est le premier cas de ce type.

À lire aussi

1 commentaires

 
GN⁺ 2024-12-22
Commentaires Hacker News

  • En migrant un projet vers Rust, j’ai tiré quelques conclusions :

    • Convertir un programme C en Rust permet de détecter les bugs plus vite grâce aux contraintes strictes de Rust.
    • La conversion automatique de C vers Rust ne résout pas tous les cas, car les deux langages reposent sur des conceptions fondamentalement différentes.
    • Dans certains cas, le portage de C vers Rust peut être impossible, car l’insécurité est intrinsèque à la conception même.
    • Les progrès des outils devraient fluidifier le processus de portage.

  • Les bases de code C formellement vérifiées et les bases de code C système ordinaires sont différentes.

  • En 2002, des chercheurs ont publié un papier sur Cyclone, un dialecte sécurisé de C, et ont découvert des bugs de sécurité en migrant du C vers Cyclone.

    • Ces migrations, qu’elles soient manuelles ou automatiques, peuvent accroître l’adoption d’un langage sûr et débusquer des bugs existants.

  • Une traduction directe vers Rust peut générer des parties sûres et des parties non sûres, et le travail manuel peut se concentrer sur la validation de la sûreté des zones non sûres.

    • Même si la partie non sûre est importante, cela peut quand même valoir le coup.

  • On attend peu d’une approche qui ne compile que de petites portions de C.

    • Parce que le modèle d’ownership de Rust est trop différent des programmes C réels.

  • Il faut s’interroger sur la comparaison avec la conversion C de Zig.

    • Zig gère bien les environnements mixtes entre code neuf et code C existant, et peut aussi servir de compilateur C.
    • On se demande pourquoi les mainteneurs du noyau Linux ne considèrent pas Zig comme un remplaçant possible de C.

  • Question de savoir si C2Rust peut produire du code formellement correct.

    • Le lien vers la source qui génère du code Rust n’est pas visible.

  • Si une bibliothèque C fonctionne, il peut être pertinent de la traduire avec l’unsafe de Rust.

    • Rust manque généralement de bibliothèques.

  • Il est intéressant que l’optimisation élevée n’améliore pas beaucoup la vitesse de Rust.

    • Curiosité sur la performance d’une compilation en une passe de C vers Rust avec l’option O3.