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
  • Scylla propose, plutôt que de porter du C existant vers du Rust unsafe puis de le corriger, un chemin consistant à structurer progressivement le C source afin de pouvoir le compiler directement en Rust sûr
  • La cible est un sous-ensemble applicatif de C couvrant le traitement de données, l’arithmétique de pointeurs, les flux de contrôle structurés et le code portable ; sont exclus les codes dépendant de goto, des conversions entier-pointeur, des astuces de pointeurs, des champs de bits et des unions non étiquetées
  • La transformation se fait en deux étapes : abaisser l’AST Clang vers Mini-C, puis le traduire en Rust sûr ; les comportements subtils de C, comme la promotion des entiers, les conversions implicites, les expressions d’affectation et les incréments préfixes/postfixes, y sont rendus explicites
  • La partie la plus délicate, l’arithmétique de pointeurs, est remplacée par des découpages fondés sur les slices Rust et split_at_mut/split_at, avec inférence de mutabilité, dérivation de traits et choix entre Box et emprunts
  • L’évaluation porte sur SymCrypt de Windows, HACL★, le cœur de l’algorithme de compression bzip2, le parseur/sérialiseur CBOR d’EverParse et une partie de Microsoft FrodoKEM ; la transformation a aussi permis de détecter des comportements indéfinis dans bzip2 et FrodoKEM

Le chemin de migration C→Rust choisi par Scylla

  • La motivation pour porter du code C existant vers Rust part des problèmes de sécurité mémoire
    • Des études de Google et Microsoft estiment que 70 % des vulnérabilités de sécurité sont liées à une mauvaise gestion de la mémoire
    • Les entreprises et les administrations encouragent l’usage de langages à sécurité mémoire comme Rust pour les systèmes critiques
  • Rust présente des avantages évidents pour le nouveau code, mais il est difficile de réécrire entièrement du code C industriel déjà testé et débogué
  • Les outils existants de conversion automatique C→Rust produisent généralement du Rust unsafe afin de prendre en charge l’ensemble de C
    • Ils autorisent des idiomes de style C comme les pointeurs non vérifiés ou la transmutation de Rust
    • Les garanties statiques de sécurité mémoire disparaissent, ce qui affaiblit l’intérêt d’utiliser un langage sûr
  • Le workflow courant consiste à prendre la sortie Rust unsafe comme point de départ, puis à la refactoriser itérativement vers du Rust sûr
    • Des analyses statiques ont été proposées pour remplacer les raw pointers par des emprunts Rust sûrs, ou pour restaurer des abstractions Rust à partir de représentations bas niveau
    • Les outils de refactoring sont dispersés, et la prise en charge de c2rust refactor a été arrêtée en 2022
  • Scylla choisit de ne pas corriger le Rust unsafe généré, mais de structurer progressivement le code C lui-même pour le rendre compilable en Rust sûr

Sous-ensemble de C pris en charge et motifs exclus

  • L’objectif de Scylla est de produire une transformation prévisible et du code Rust proche du C source
  • La cible est un sous-ensemble applicatif de C
    • Du code qui manipule et traite des données
    • Du code qui utilise l’arithmétique de pointeurs
    • Du code doté d’un flux de contrôle structuré
    • Du code portable
  • Les bases de code qui dépendent des motifs suivants ne sont pas prises en charge
    • goto
    • L’utilisation de la représentation des objets via des conversions entier-pointeur
    • Les astuces de pointeurs
    • Les champs de bits
    • Les unions non étiquetées
  • Les développeurs peuvent appliquer au code source C des réécritures ciblées et des annotations afin que Scylla puisse le comprendre
    • Les motifs d’aliasing incompatibles avec le borrow checker de Rust peuvent être réécrits
    • Il est possible de fournir à Scylla l’information selon laquelle une union étiquetée doit être traduite en ADT de haut niveau

Mini-C : un langage intermédiaire qui réduit les ambiguïtés de C

  • Scylla part de l’AST du frontend Clang et le transforme d’abord en un langage appelé Mini-C
  • Mini-C traite, comme C, les branchements, les boucles, les pointeurs, le déréférencement et la prise d’adresse, mais avec une sémantique « sans surprise »
    • Tous les entiers ont une largeur fixe
    • Les integer promotions et integer conversions de C sont représentées par des casts explicites
    • Les pointeurs non typés comme void * ne sont pas autorisés
  • Contrairement à C, Mini-C est un langage d’expressions
    • L’affectation ne renvoie pas de valeur
    • Les constructions C comme e1 = e2 = e3 ou p[i++] sont désucrées en Mini-C
    • Les expressions de test des boucles et des conditions doivent être de type bool, et non du type int de C
  • Lors du passage de l’AST typé de Clang à l’AST typé de Mini-C, les comportements implicites de C sont rendus explicites
    • Les conditions sont ajustées en bool
    • Les indices de tableau sont ajustés en size_t
    • Les conversions implicites des arguments d’appel de fonction et des membres droits d’affectation sont transformées en casts explicites
    • Les opérations arithmétiques reflètent les usual arithmetic conversions du standard C
  • La transformation suppose que le code C est portable et ne dépend pas du modèle de données C
    • Par exemple, elle ne s’attend pas à du code dont le comportement change selon que long fait 4 ou 8 octets
    • L’implémentation détecte au moment de la configuration le modèle de données de l’architecture cible et convertit unsigned int en type à largeur fixe comme uint32_t

Synthèse d’ADT et de tuples

  • Mini-C fournit des ADT, des tuples et du pattern matching de plus haut niveau que C
  • Les unions étiquetées sont traduites en ADT au moyen d’annotations
    • La forme cible est une structure du type { int tag; union { t0 case0; ...; tn caseN }}
    • Les valeurs de tag vont de 0 à N, et l’on suppose qu’elles correspondent à l’ordre des cases dans l’union
  • Scylla transforme les types d’union étiquetée annotés en types variants
    • Lors de la création d’une valeur, il vérifie que .tag = i et .casej = e correspondent
    • S’ils correspondent, il les convertit en la valeur du constructeur correspondant
    • Si le payload et le tag ne correspondent pas, il ne traduit pas en Mini-C
  • L’accès aux champs d’une union étiquetée n’est sûr que si l’on connaît l’état courant du tag
    • Il reconnaît des motifs comme if (x.tag == i) { ... x.casei } ou switch
    • Il les transforme en une forme match x with | Ci v -> ...
    • Les accès à une autre case de l’union sont considérés comme invalides et provoquent une erreur de conversion
  • Les tuples peuvent aussi être synthétisés par annotation
    • Une struct à n champs est transformée en tuple n-aire
    • Les accès aux champs deviennent des accès à des champs de tuple
    • Les tuples sont typés structurellement et peuvent bénéficier du mut-polymorphism

Transformation de Mini-C vers Rust sûr

  • Mini-C fournit une représentation de programme C avec des annotations de type complètes, qui est ensuite transformée en Rust sûr
  • Les principales difficultés sont au nombre de trois
    • Éliminer l’arithmétique de pointeurs de C
    • Expliciter la mutabilité et l’aliasing
    • Fournir automatiquement des structures idiomatiques de Rust comme les traits
  • La transformation des types pointeurs est complexe en raison des différences de représentation des pointeurs en Rust
    • Rust distingue Box<T> et &T
    • Il distingue aussi les pointeurs vers un seul élément et les pointeurs vers plusieurs éléments, comme &T et &[T]
    • Les tableaux Rust sont des valeurs et ne se dégradent pas automatiquement en pointeurs comme en C
  • La stratégie de base consiste à compiler tous les pointer types de C en emprunts de slice Rust &[T]
    • Les pointeurs de pile comme les pointeurs de tas deviennent par défaut des emprunts de slice
    • Les pointeurs vers un seul élément comme ceux vers plusieurs éléments deviennent aussi par défaut des emprunts de slice
    • La mutabilité est inférée automatiquement dans une étape distincte
  • Scylla traduit certains pointeurs en Box<T> au moyen d’heuristiques et d’annotations manuelles
    • Une fonction comme T *create(), sans référence globale et considérée comme une fresh allocation, peut être traduite en fn create() -> Box<T>
    • Cette analyse est appliquée récursivement par point fixe jusque dans les définitions de structs et de variants
    • Les structs où subsistent des emprunts reçoivent un paramètre de lifetime

Contraintes de conversion entre Box, slice et array

  • Comme Rust exige des conversions explicites entre tableaux, emprunts de slice et Box, la transformation Rust de Scylla fonctionne elle aussi de manière orientée types
  • Les règles de transformation insèrent des coercions qui convertissent un tableau ou une slice boxed en emprunt de slice
    • Un tableau devient un emprunt de slice sous une forme comme &x[..]
    • Une slice boxed peut être convertie en emprunt
  • La conversion inverse est également possible
    • Une slice ou un tableau peut être promu en allocation sur le tas et devenir Box<[T]>
  • Cette conversion inverse peut créer une différence de sémantique de copie
    • En C, un tableau et un pointeur peuvent désigner la même mémoire
    • En Rust, Box::new(x) peut créer une copie de x
    • Pour les tableaux de types primitifs comme les tableaux d’entiers, il n’existe pas de moyen de se retirer du trait Copy, si bien que Rust peut effectuer silencieusement une copie
  • Lorsqu’une telle conversion se produit, Scylla retire la variable d’origine de l’environnement afin d’interdire toute utilisation ultérieure
    • Si le programme C source continue à utiliser cette variable, une erreur de conversion est produite
    • Le développeur doit corriger le code source C avant la transformation afin de clarifier l’intention

Remplacer l’arithmétique de pointeurs par un découpage de slices Rust

  • Les programmes C n’accèdent souvent pas à un tableau au moyen d’un seul pointeur de base : ils le découpent en chunks ou le parcourent en conservant un pointeur sur la position courante
  • Rust n’autorise pas l’arithmétique arbitraire de pointeurs et propose à la place de diviser une slice avec split_at_mut ou split_at
    • split_at_mut est une primitive qui abandonne la possession de la slice d’origine et obtient deux sous-slices
    • Elle maintient l’invariant Rust selon lequel des données mutables doivent avoir un propriétaire unique
  • Scylla introduit un split tree pour faire correspondre l’arithmétique de pointeurs C à la méthode de découpage de Rust
    • Chaque pointeur C est associé à un split tree
    • Le split tree change de manière flow-dependent
    • Il suit, à un point donné du programme, quel accès à une slice Rust doit remplacer un accès par pointeur C
  • Comme les pointeurs C ne portent pas d’information de longueur, Scylla suppose que les chunks ne se chevauchent pas
    • Si un chevauchement est intentionnel, le code ne peut pas passer la vérification de types de Rust, et le développeur doit réécrire le code C
    • Pour que la transformation reste prévisible, elle évite le backtracking et procède en avant
  • Dans l’exemple, un tableau de 32 octets abcd est découpé en quatre zones limb de 8 octets
    • En C, l’arithmétique de pointeurs se fait dans un ordre qui n’est pas de gauche à droite, comme abcd + 0, abcd + 16, abcd + 8, abcd + 24
    • La transformation Rust conserve l’historique des appels à split_at_mut dans un split tree afin de retrouver la bonne sous-slice

Cibles d’évaluation et comportements indéfinis découverts

  • L’implémentation de Scylla utilise Clang pour prendre en entrée du code C existant et produire du Rust sûr
  • L’évaluation inclut des parties de plusieurs projets C existants
    • Une partie de SymCrypt sous Windows
    • Une partie de la bibliothèque cryptographique HACL★
    • Les parties centrales de l’algorithme de compression bzip2
    • Le parseur et le sérialiseur binaires CBOR de la bibliothèque EverParse
    • L’implémentation par Microsoft de la primitive cryptographique post-quantique FrodoKEM
  • Ces cas montrent que le sous-ensemble applicatif de C de Scylla peut couvrir plusieurs applications sensibles à la sécurité
  • Lors de la transformation, des comportements indéfinis présents dans le code C source de bzip2 et de FrodoKEM ont aussi été identifiés et signalés

À lire aussi

1 commentaires

 
GN⁺ 2024-12-22
Avis sur Hacker News

  • Il est important de noter que ce travail cible « des bases de code C déjà formellement vérifiées »
    Le C système ordinaire n’est pas formellement vérifié, c’est donc une histoire assez différente

    • Malgré cela, cela ne semble pas totalement fiable. La section 2.2 de l’article indique aussi que les coercitions introduites par les règles de transformation peuvent créer de subtiles différences de sémantique
      Par exemple, un pointeur vers un tableau C sur la pile peut être traduit en Rust comme un pointeur possédant une nouvelle copie sur le tas, de type Box<[u8]>. Si le code d’origine s’appuyait sur le fait que le pointeur pointait réellement vers le tableau, le code traduit pourrait se comporter silencieusement de façon incorrecte
      La fonctionnalité de traduction automatique du sous-ensemble C++ sûr en mémoire de mon projet scpptool aurait traité cela en déplaçant les tableaux vers des types de remplacement et des itérateurs, de manière à préserver la sémantique d’origine
      Il se peut que le projet de l’OP ne traite que le C facile à convertir en Rust sûr, mais vu la difficulté du problème, le résultat mérite le respect et semble avoir une certaine utilité
    • Il y a beaucoup plus de réserves que cela, et on est presque dans le discours marketing exagéré
      Pour commencer, ils n’ont pas traduit du vrai C : ils ont modifié du code écrit en F* pour que le compilateur C émette du Rust. Ils ne se sont pas attaqués à du C réel complexe ; au mieux, ils ont traité un Mini-C limité, du genre de ce que produirait un compilateur jouet
      Le texte original dit aussi que si le programme C d’origine dépend davantage de x, la traduction signale une erreur et demande au programmeur de modifier la source, ce qui signifie qu’ils espèrent que le C a déjà été écrit dans un style satisfaisant le vérificateur d’emprunts de Rust
      Cela ressemble à une formulation académique du type « la figure 4 présente de belles règles, mais l’implémentation réelle repose sur une multitude d’astuces »
      Pire encore, il est dit que les chevauchements distinguables statiquement produisent une erreur de compilation, tandis que dans les autres cas le code Rust peut paniquer à l’exécution. Transformer un programme C formellement vérifié en programme Rust qui « peut désormais crasher » est étrange
      Il est également inexact de qualifier HACL* de base de code C formellement vérifiée existante. HACL* compile bien vers C, mais ce n’est pas une bibliothèque C : elle est écrite dans un langage totalement différent
      Un titre honnête aurait dû être quelque chose comme « Compiler un sous-ensemble de F* vers du Rust partiellement sûr, partiellement formalisé »
    • Rust lui-même est-il formellement vérifié ? À ma connaissance, non
    • Je me demande ce qu’est exactement du C formellement vérifié, et pourquoi il n’y en a pas davantage
    • Je me demande quelle est la différence essentielle. Peut-on imposer la conformité avec des flags de compilateur ?

  • En 2002, des chercheurs ont publié un article sur Cyclone, un dialecte sûr de C, et en portant manuellement du code C vers Cyclone, ils ont découvert des bugs de sûreté dans du code C existant
    Ces transformations de C, manuelles ou automatiques, ont le potentiel non seulement d’accroître l’adoption de langages plus sûrs, mais aussi de révéler des bugs existants
    [1] https://www.researchgate.net/profile/James-Cheney-2/publicat...

    • Cyclone n’est plus maintenu, le projet de recherche principal est terminé, et les développeurs sont passés à autre chose
      Plusieurs idées de Cyclone ont été intégrées à Rust, et le code peut être remis en état de marche avec des efforts, mais il ne se compile pas directement sur les plateformes 64 bits modernes
      http://cyclone.thelanguage.org

  • J’ai porté quelques projets vers Rust, dont des projets en C, en utilisant C2Rust comme première étape, et j’en ai tiré quelques conclusions

    1. Quand on migre un programme C vers Rust, même avec du unsafe, les contraintes fortes de Rust — par exemple les vérifications de bornes et les signatures strictes — font souvent apparaître les bugs rapidement
    2. Je ne pense pas que la conversion automatique de C vers Rust puisse être entièrement résolue. La conception d’un programme C est fondamentalement différente de celle d’un programme Rust, et le rendre sûr nécessite une refonte importante
    3. Dans certains cas, il est impossible de passer de C à Rust en préservant exactement la sémantique. C’est parce que l’insécurité peut être inhérente à la conception elle-même
      Malgré tout, les outils sont indispensables pour le portage, et plus ils progresseront, plus le processus deviendra fluide
    • Convertir automatiquement vers du « Rust rapide et sûr » est difficile, mais convertir automatiquement vers du Rust sûr au sens général est beaucoup plus facile
      Il suffit de représenter la mémoire sous forme de tableau et de traiter les pointeurs comme des indices dans ce tableau. Cela permet d’exprimer des comportements de C comme l’arithmétique de pointeurs non vérifiée ou les unions sans se battre avec le vérificateur d’emprunts, tout en préservant la sémantique. Des techniques similaires sont utilisées depuis longtemps pour C→Java
      Bien sûr, la valeur d’une telle conversion est ambiguë. En pratique, cela ressemble à compiler du C vers wasm, mais en plus lent ; et même si le code résultant est techniquement « sûr », il reste des problèmes comme les débordements de tampon qui créent un état incorrect, ou les pointeurs pendants qui permettent d’accéder à des données dans des contextes où cela ne devrait pas être autorisé
    • Je suis d’accord en principe avec l’idée que « l’insécurité peut être inhérente à la conception », et mon expérience me le fait aussi ressentir fortement, mais j’aimerais avoir un exemple simple pour rendre la discussion plus concrète

  • Je suis l’auteur. Il me semble utile de clarifier quelques points évoqués dans plusieurs fils

    1. Il s’agit d’un article de recherche mis sur arXiv, pas de l’annonce d’un nouveau produit prétendant résoudre le problème C→Rust. Il a été soumis à une conférence PL, et le public comme les attentes ne sont pas les mêmes que pour une présentation dans un événement open source comme FOSDEM
    2. L’approche est simple. En partant de la contrainte consistant à traduire du C en Rust sûr, nous examinons la nécessité d’un petit sous-ensemble de C qui fonctionne bien, de l’inférence de découpage de slices, de traductions pouvant échouer, de programmes pouvant être interrompus, etc. Nous l’avons évaluée sur la cible dont nous disposons, à savoir du C intégré dans F*, et nous avons montré que, sous cette contrainte, elle passe assez bien à l’échelle sur de grandes bibliothèques C utilisées dans des logiciels grand public comme Firefox ou Python. Nous ne prétendons pas pouvoir réécrire automatiquement Firefox en Rust
    3. La recherche fonctionne comme ça. Nous pensons avoir identifié un point intéressant dans l’espace de conception ; nous ne prétendons pas résoudre tous les problèmes, mais estimons que c’est une idée susceptible d’ouvrir la voie à de nouveaux progrès dans la traduction C→Rust. Un outil existant pourrait utiliser cette approche pour le code qui correspond au sous-ensemble visé, et se rabattre sur de l’unsafe Rust pour les parties qui ne conviennent pas
    4. Ce n’est pas la version finale. Nous sommes en train de construire un vrai frontend C avec libclang, et nous explorons aussi des moyens de garantir que le Rust généré ne produise pas d’accès hors limites. Par exemple, nous envisageons d’émettre des conditions de vérification vers Z3. Si les reviewers estiment qu’il faut davantage de travail, nous améliorerons puis soumettrons à nouveau ; et s’ils jugent que le domaine est actif et que d’autres peuvent tirer profit des idées, et acceptent l’article, ce sera encore mieux

  • Ce que je me demande vraiment, c’est pourquoi procéder ainsi
    S’il s’agit d’une technologie capable de convertir réellement des applications industrielles de C vers Rust, elle devrait aussi permettre de blindage plus facilement les applications C existantes. Il suffirait de produire l’analyse à intégrer à des outils existants comme des analyseurs statiques ou des générateurs de tests
    De même, on pourrait générer des wrappers sûrs afin d’écrire le nouveau code en Rust à côté du C vérifié. Le nouveau code bénéficie des avantages de Rust, le code existant est confirmé comme sûr, et l’interface devient elle aussi plus sûre
    Un traducteur complet peut être idéal. À long terme, il est en effet préférable qu’une base de code soit dans un seul langage. Mais pour le C/C++ existant, le besoin le plus important reste une amélioration de la sûreté en un clic avec peu de faux positifs. Il pourrait aussi être possible de corriger automatiquement les mauvaises structures dans le C, comme le font les outils de compilation de Google ou Mayhem de ForAllSecure

    • Certains programmes C ne peuvent pas être rendus sûrs ; l’affirmation selon laquelle « une technologie capable de convertir des applications industrielles en Rust pourrait rendre plus facile le blindage des applications C » n’est donc pas correcte
      Cela peut être parce qu’ils dépendent d’un comportement indéfini ou non spécifié, ou parce que l’ajout de contrôles de sûreté appropriés réduirait tellement l’espace des entrées acceptables qu’ils deviendraient inutiles
      Les traduire vers un langage sûr est objectivement meilleur dans ces cas, car cela permet de conserver l’expressivité des entrées tout en garantissant statiquement un comportement correct à l’exécution
      Quant au « C éprouvé sur le terrain », il est difficile de considérer qu’il existe, comme le montrent les innombrables vulnérabilités critiques. Ce qui existe réellement, c’est du C qui fonctionne assez bien, assez souvent, pour paraître utile
      Le vieux code est supposé sûr par chance, il n’est pas prouvé. Le mot « preuve » a un sens particulier, surtout dans le contexte de ce genre d’article, et l’écrasante majorité du code C n’est pas prouvée selon des critères mathématiques rigoureux. En revanche, la correction du système de types de Rust est prouvée mathématiquement
      Un traducteur complet dépend de ce que l’on est prêt à sacrifier. Si l’on peut renoncer aux performances, à l’espace des entrées, à l’étendue des sorties, à la lisibilité du code, etc., c’est possible dans une certaine mesure ; mais les problèmes commencent dès qu’on veut un traducteur à la fois sain et complet sur tous ces aspects

  • Une traduction naïve vers Rust ne produirait-elle pas un mélange de parties sûres et de parties unsafe ? Dans ce cas, le travail manuel consisterait seulement à vérifier la sûreté des zones unsafe. Ce serait similaire au fait d’écrire du Rust dès le départ
    Si 90 % du résultat n’est pas unsafe, cela semble pouvoir être un gain appréciable

    • C’est effectivement le cas. Quelqu’un a déjà essayé de convertir OpenJPEG avec c2rust en unsafe Rust bas niveau
      OpenJPEG était connu pour provoquer une segfault sur un cas de test précis, et lorsque ce test a été exécuté sur la version Rust, une segfault s’est produite dans le code Rust correspondant au même endroit. Au moins, la compatibilité était là
      Mais cette approche est une impasse. Pour progresser, le traducteur doit reconnaître les idiomes courants du C et les remonter vers les formes naturelles du langage cible. « Compiler » vers Rust produit du Rust épouvantable, rempli d’appels à des fonctions de manipulation de pointeurs façon C et non sûres
      Le plus gros problème de remontée concerne surtout les pointeurs. Le résultat le plus prometteur de cet article est d’avoir trouvé une méthode pour transformer l’arithmétique de pointeurs C en slices Rust. Les slices peuvent faire la plupart de ce que fait l’arithmétique de pointeurs en C, et quelqu’un a maintenant automatisé cette traduction. L’arithmétique de pointeurs qui ne peut pas être traduite doit être considérée avec beaucoup de suspicion
      Il est utile de considérer qu’en C, un pointeur brut vers un tableau porte implicitement une longueur. Cette longueur n’apparaît pas dans le source C, mais elle existe quelque part comme fonction de l’état du programme. Elle peut être une constante, la taille demandée à malloc, ou un paramètre de fonction. Pour un programmeur chargé de la maintenance, retrouver la longueur d’un tableau n’est généralement pas très difficile
      C’est peut-être un problème bien adapté aux LLM. On pourrait demander « en regardant ce code, quelle est la longueur du tableau foo ? », puis laisser un traducteur non LLM guider la conversion vers Rust. Si le LLM se trompe, Rust déclenchera une erreur d’indexation ou se retrouvera avec un tableau trop grand, mais ce ne sera pas dangereux. Les idiomes C pour l’information de taille des tableaux sont assez structurés pour être correctement devinés la plupart du temps. En particulier, les LLM peuvent aussi lire les commentaires
    • Une traduction naïve produira presque entièrement du code Rust unsafe, parce qu’elle utilisera partout des pointeurs bruts au lieu de références
      Le code C n’étant pas écrit en tenant compte du modèle d’aliasing de Rust ni des contraintes du borrow checker, il est difficile de le traduire en références

  • Il ne s’agit que de compiler un très petit sous-ensemble de C. En pratique, il pourrait même être si réduit qu’il en serait inutile
    J’ai peu d’attentes pour cette approche. Elle se heurtera forcément aux limites de ce que permet l’analyse statique du code C. En plus, le choix de Rust comme cible rend le problème inutilement difficile. Le modèle de propriété de Rust est trop différent de la façon dont les programmes C réels fonctionnent

    • Le modèle de propriété de Rust est suffisamment proche pour traduire du C. Il est simplement plus explicite et plus fortement typé, donc le traducteur doit comprendre ce que du code C libre cherche à faire et le mapper vers des idiomes Rust
      Par exemple, les buffers en C ont évidemment une longueur, mais en C cette longueur n’est pas explicitement liée au pointeur. Le traducteur doit donc inférer comment le programme C suit cette longueur et la convertir en slice. Ce n’est déjà pas simple quand la longueur est une variable explicite, et c’est encore plus délicat si elle est calculée ou si la représentation devient un pointeur “juste après la fin”
      Des patterns C comme bool should_free_this_pointer peuvent aussi être transposés en enum Owned/Borrowed de Rust, mais il faut inférer quelle allocation est liée à quel booléen, et quelle est la vraie plage de sûreté de la variante empruntée
    • Cela peut être intéressant comme langage d’interface. Utile pour les bindings
    • Au final, j’ai l’impression que les gens vont y jeter des LLM et dire que ce n’est pas grave s’ils hallucinent en masse du code vaguement correct
      Cela dit, je suis d’accord qu’il sera difficile de produire du Rust idiomatique à partir de C arbitraire. Disons que ce sera du “à peu près correct”

  • Je me demande comment cela se compare à la fonction de conversion C de Zig
    Zig semble excellent pour créer des environnements mixtes où le nouveau code est en Zig et l’ancien reste en C, faire de la conversion ou de l’interopérabilité, et même servir de compilateur C
    Il doit y avoir de très bonnes raisons pour lesquelles les mainteneurs du noyau Linux ne voient pas Zig comme un remplaçant de C plutôt que Rust. Je n’en sais pas assez pour spéculer, donc j’aimerais que des personnes plus au fait l’expliquent

    • Rust est moins un “remplaçant de C” qu’un outil ajouté à C. C’est un outil dont Torvalds et d’autres ont reconnu la valeur et qu’ils ont autorisé dans le noyau, tandis que la majeure partie du code du noyau continuera d’être écrite en C
      Je ne suis pas mainteneur du noyau, mais si je devais deviner deux grandes raisons pour lesquelles Rust a été choisi plutôt que Zig, ce pourrait être les meilleures garanties à la compilation offertes par le langage et sa vitesse d’adoption
      De grandes entreprises du secteur font beaucoup d’efforts pour fournir du code natif Rust pour leurs API ou des bindings Rust maintenus. Les développeurs Windows réécrivent aussi certaines parties de leur propre noyau en Rust. C’est un mouvement qui dure depuis un bon moment, et j’espère qu’il ne s’arrêtera pas
      Les mainteneurs peuvent aussi estimer que Zig n’apporte pas assez d’avantages par rapport à C. Beaucoup d’entre eux restent d’ailleurs opposés même à Rust
    • D’après ce que je comprends, la plupart des mainteneurs du noyau ne cherchent pas à remplacer C par quoi que ce soit
      Zig a une interopérabilité bien meilleure avec C que Rust, mais il n’est pas memory safe et n’est pas stabilisé. L’adoption de Zig dans le monde C va probablement beaucoup progresser, mais il est difficile de dire qu’il concurrence directement Rust
      Dans ma région, personne n’adopte Rust, et les gens du C++ restent sur C++. Il y a eu un peu d’intérêt pour Rust au début, mais il ne s’est imposé dans aucune entreprise que je connais. C’est sans doute pour des raisons similaires au fait que Go a fortement progressé dans les jeunes entreprises, mais a du mal à pénétrer les entreprises Java/C# traditionnelles. Même quand cela a du sens techniquement, c’est un énorme défi de conduite du changement
      Zig gagne du terrain du côté des programmes qui n’ont pas besoin d’allocation mémoire dynamique, mais pas beaucoup au-delà
    • Zig n’est pas encore assez mature pour être envisagé dans le noyau
      Il y a encore régulièrement des changements cassants, ce qui est positif pour Zig aujourd’hui, mais pas pour une base de code aussi énorme et durable que Linux. Il y a aussi des bugs de compilateur
      Je dis cela en appréciant globalement la direction prise par Zig
    • Zig n’est pas encore en 1.0 et n’offre aucune garantie de rétrocompatibilité. Il n’est presque utilisé nulle part et, même si certains aspects semblent prometteurs, il n’a pas encore prouvé sa valeur
    • C’est peut-être parce que Zig n’est pas memory safe

  • Je me demande si des outils comme C2Rust pourraient s’appuyer dessus pour générer du code formellement correct
    Je me demande aussi quelle part les auteurs ont faite à la main, ou s’ils ont lancé quelque chose pour générer le code Rust. Dans ce cas, je ne vois pas où se trouve le code qui génère le Rust, ni de lien vers le dépôt source

    • L’article indique qu’après la fin du processus de revue, donc globalement après la publication officielle de l’article, ils publieront ces développements sous licence open source

  • Si une bibliothèque C fonctionne, c’est-à-dire qu’elle n’a pas été formellement prouvée exempte de problèmes mais qu’elle marche correctement dans la plupart des cas, je me demande pourquoi ne pas la traduire en utilisant unsafe Rust
    Vu le manque général de bibliothèques en Rust, je pense que cela aurait de la valeur. Au fond, ce n’est pas très différent d’utiliser une dll/so écrite en C, qui peut être unsafe dans certaines situations