Vérification formelle en traduisant les crates core et alloc de Rust en Coq

 (formal.land)
1 points par GN⁺ 2024-05-16 | 1 commentaires | Partager sur WhatsApp
  • coq-of-rust, qui transpose les programmes Rust en Coq, commence à couvrir les crates core et alloc de la bibliothèque standard, ce qui réduit la charge liée à l’écriture manuelle de définitions Coq pour chaque fonction primitive
  • Ces deux crates sont de vastes bases de code contenant beaucoup de code unsafe et de Rust avancé ; l’enjeu central est donc de traiter le résultat de la traduction automatique comme des unités compilables et vérifiables
  • En découpant la sortie par fichier Rust d’entrée, alloc représente 54 fichiers et 171 783 lignes, tandis que core représente 190 fichiers et 592 065 lignes, ce qui facilite la compilation parallèle et le débogage
  • Les collisions de noms de modules dans les blocs impl ont été atténuées en incluant les informations des clauses where, mais 4 % des fichiers ne compilent toujours pas actuellement en Coq
  • L’exemple Option::unwrap_or_default illustre une méthode consistant à prouver l’équivalence entre la définition traduite automatiquement et une définition fonctionnelle plus simple, ce qui nécessite à la fois de faire confiance à l’automatisation et de vérifier au moment de la preuve

Traitement des primitives de la bibliothèque standard Rust

  • Formal Land développe coq-of-rust, qui traduit les programmes Rust vers le système de preuves formelles Coq
  • Jusqu’ici, pour traiter les composants primitifs de la bibliothèque standard Rust, il fallait créer séparément une définition Coq décrivant le comportement de chaque fonction
  • Pour réduire cette charge, les crates core et alloc de Rust ont été traduites avec coq-of-rust
  • Le résultat de la traduction est consultable aux emplacements suivants

Résultats de la première exécution de la traduction

  • Lors de la première exécution de coq-of-rust sur alloc et core, deux fichiers Coq de plusieurs centaines de milliers de lignes ont été générés, chacun correspondant à l’intégralité d’une crate
  • Cela a confirmé que l’outil pouvait s’exécuter sur de grandes bases de code, mais le code Coq généré ne compilait pas immédiatement
  • Les erreurs étaient rares, mais apparaissaient environ une fois toutes les quelques milliers de lignes
  • Selon cloc, la taille du code Rust d’entrée était la suivante
    • alloc : 26 299 lignes de code Rust
    • core : 54 192 lignes de code Rust
  • Comme une expansion des macros a lieu pendant la traduction, la cible réellement traduite est plus grande que le nombre de lignes d’origine

Découpage du code Coq généré

  • Le principal changement a consisté à découper la sortie de coq-of-rust en un fichier Coq par fichier Rust d’entrée
  • Ce découpage a été possible parce que la traduction est insensible à l’ordre des définitions et context-free
  • Les fichiers Rust ont généralement des dépendances cycliques entre eux, ce que Coq n’autorise pas, mais cette approche de traduction permet une séparation par fichier
  • Après découpage, la taille de la sortie est la suivante
    • alloc : 54 fichiers Coq, 171 783 lignes de code Coq
    • core : 190 fichiers Coq, 592 065 lignes de code Coq
  • Le découpage en fichiers facilite l’exploration et la maintenance du code généré
    • Il devient plus simple de paralléliser la compilation
    • On peut déboguer en se concentrant sur un fichier à la fois
    • Il est plus facile d’exclure les fichiers qui ne compilent pas
    • Il devient plus simple de suivre le diff d’un fichier unique

Correction des collisions de noms de modules et fichiers restants

  • Certains bugs provenaient de collisions de noms de modules dans les blocs impl
  • La solution a consisté à augmenter l’unicité des noms de modules en y ajoutant davantage d’informations
    • Les informations des clauses where, auparavant absentes, sont désormais incluses
    • Par exemple, dans l’implémentation du trait Default pour Mapping<K, V>, la condition selon laquelle K et V doivent tous deux implémenter Default est reflétée dans le nom du module
  • Les fichiers qui ne compilent pas actuellement en Coq sont les suivants
    • alloc/boxed.v
    • core/any.v
    • core/array/mod.v
    • core/cmp/bytewise.v
    • core/error.v
    • core/escape.v
    • core/iter/adapters/flatten.v
    • core/net/ip_addr.v
  • Cela correspond à 4 % de l’ensemble des fichiers
  • Même dans les fichiers qui compilent, certains composants Rust non encore pris en charge sont axiomatisés ; ce seul pourcentage ne suffit donc pas à évaluer toute l’étendue des éléments non pris en charge

Exemple de traduction de Option::unwrap_or_default

  • En Rust, Option::unwrap_or_default renvoie x si la valeur est Some(x), et appelle T::default() si elle est None
  • coq-of-rust traduit cela en une définition Coq de forme monadique
    • Elle fait correspondre les arguments d’entrée et les types
    • Dans la branche Some, elle récupère le champ du tuple et le copie
    • Dans la branche None, elle appelle la méthode default du trait core::default::Default
  • Dans la vérification réelle, une définition fonctionnelle plus simple est utilisée à la place de la définition générée automatiquement
    • Si la valeur est None, elle renvoie core.simulations.default.Default.default
    • Si la valeur est Some x, elle renvoie x
  • La preuve d’équivalence entre la définition générée automatiquement et la définition simple se trouve dans CoqOfRust/core/proofs/option.v
  • Si le code Rust d’origine change, cette preuve permet de détecter le changement
  • Comme la traduction de la bibliothèque core est automatique, la définition générée peut être jugée plus fiable qu’une définition écrite à la main
  • Toutefois, coq-of-rust peut lui aussi comporter des erreurs ou des incomplétudes ; il faut donc vérifier au moment de la preuve que le code est valide

Travaux restants

  • La confiance dans la formalisation de la bibliothèque standard pour la vérification de programmes Rust s’en trouve renforcée
  • Le prochain objectif reste la simplification du processus de preuve, encore fastidieux
  • En particulier, pour montrer qu’une simulation est équivalente au code Rust d’origine, les tâches suivantes sont nécessaires
    • Résolution des noms
    • Introduction de types de haut niveau
    • Élimination des effets de bord
  • Traiter ces étapes séparément constitue la direction des améliorations à venir

À lire aussi

1 commentaires

 
GN⁺ 2024-05-16
Avis de Hacker News

  • Vraiment impressionnant.
    Ce genre de traduction automatique déplace l’objet de la confiance vers l’outil. coq-of-rust lui-même est écrit en Rust, pas en Coq, donc la structure récursive est assez étonnante ; mais en combinant une approche à la CompCert avec une manière de contourner l’attaque Trusting Trust de Ken Thompson au moyen d’un second compilateur, comme dans « Countering Trusting Trust through Diverse Double-Compiling » (2009) de David A. Wheeler [0], une preuve de correction semble possible.
    Pour le vérifier, il suffirait de convertir le traducteur coq-of-rust de Rust vers Coq avec coq-of-rust ; même si cette traduction a été effectuée en Rust et qu’on ne lui fait donc pas confiance, il reste à prouver dans Coq les propriétés de correction voulues, en particulier que la traduction d’un programme Rust vers Coq préserve la sémantique.
    Comme dans l’article, il sera probablement plus facile de prouver les choses sur des définitions plus fonctionnelles que les définitions générées ; il suffira donc de passer par une preuve d’équivalence entre définitions, comme on le fait dans la bibliothèque standard. Si le traducteur coq-of-rust actuel, en particulier lib/ [1], fait 6 350 lignes de Rust, écrire tout le traducteur en Coq et prouver son équivalence avec la version générée semble aussi réaliste.
    Ensuite, si l’on exécute la version Coq prouvée de coq-of-rust sur le code source Rust de coq-of-rust, les définitions Coq produites devraient coïncider avec la sortie du traducteur coq-of-rust en Rust utilisé au départ.
    À part ça, c’est agréable de voir un financement industriel pour ce genre de travail. Je suis plutôt cynique vis-à-vis des cryptomonnaies, mais il est vrai que leurs exigences de correction poussent à améliorer des domaines qui m’intéressent, comme Rust, Coq et le soutien à des étudiants de master que je connais.
    [0]: https://dwheeler.com/trusting-trust/wheelerd-trust.pdf
    [1]: https://github.com/formal-land/coq-of-rust/tree/main/lib

    • Je suis l’un des auteurs, et en effet, une telle procédure pourrait être une bonne méthode pour la vérification de coq-of-rust.
      Cela dit, même si le code lui-même est court, il dépend du compilateur Rust pour parser et typer le code Rust en entrée. Il faudrait donc aussi vérifier cette partie, ou au minimum en donner une spécification formelle sans preuve. Le fait que l’API de rustc soit assez vaste et instable est un obstacle, mais cela pourrait quand même être un moyen d’accroître la confiance.
    • Cela me rappelle l’époque où je travaillais avec SPARK Ada. Sur des projets sans cible Ada prise en charge, en particulier sur de très petits appareils, on convertissait souvent Ada en C avant de compiler pour la cible en question, ce qui permettait à SPARK d’effectuer plusieurs formes d’analyse statique.
      Bien sûr, cela introduisait le problème de devoir vérifier la sortie ou le convertisseur, mais le code C obtenu était assez lisible à des fins de vérification, son style était restreint, et le niveau de confiance dans les outils était élevé. L’analyse statique de SPARK faisait partie de l’ensemble du processus de vérification et de validation, tandis que les tests et d’autres activités apportaient des couches de confiance supplémentaires. Dans l’ensemble, c’était une approche qui fonctionnait plutôt bien.
    • Si les cryptomonnaies aident ce genre de travail, c’est certes en raison des contraintes de correction, mais aussi parce qu’une grande quantité de richesse a été transférée à des personnes intéressées par l’informatique.
      Elles dépensent cet argent dans la recherche en informatique non seulement parce que cela leur profite, mais aussi parce que c’est une forme de philanthropie liée à leurs centres d’intérêt.
    • Je ne vois pas très bien comment cette approche empêche le compilateur Rust utilisé pour produire le binaire d’injecter une charge utile malveillante. On peut construire A avec B, puis B avec A, et comparer les binaires, certes.
      Une autre approche serait le code porteur de preuve. Le compilateur Rust émettrait en plus une preuve Coq montrant que l’exécutable produit correspond à la sémantique du code source en entrée.
      Bien sûr, on pourrait aussi écrire un compilateur pour un sous-ensemble de Rust, par exemple sans borrow checker ni optimisations, vers le langage machine d’une architecture donnée, puis tout amorcer à partir de là.

  • Les programmes vérifiés de bout en bout avec un système de preuve déductive semi-automatique comme Coq sont de petite taille. Les bibliothèques peuvent être plus faciles, car le degré d’interaction entre les morceaux de code y est plus faible, mais ce n’est pas le cas des programmes ordinaires.
    En pratique, la taille des programmes vérifiables de cette manière a augmenté plus lentement que la taille moyenne des programmes dans leur ensemble. La vérification logicielle solide, c’est-à-dire montrer une conformité à 100 % avec la spécification, est évidemment utile pour des choses comme les preuves de correction d’algorithmes centraux, mais elle passe mal à l’échelle.
    C’est aussi pour cela qu’une partie de la recherche s’est déplacée vers des méthodes non solides. Le coût d’une garantie à 100 % peut être dix fois supérieur à celui d’une garantie à 99,9999 %, et l’écart de probabilité peut devenir inférieur à la probabilité de défaillances extérieures au logiciel. Les systèmes physiques ne peuvent de toute façon pas être prouvés conformes à leur spécification, et il existe aussi une probabilité que la spécification elle-même ne corresponde pas suffisamment à la réalité.

    • Le point essentiel est qu’en prouvant les parties unsafe de la bibliothèque standard ainsi que les garanties de sûreté de Rust, on peut prouver par transitivité la sûreté mémoire, l’absence de data races, etc., de tout code Rust sûr qui utilise uniquement la bibliothèque standard.
      Prouver que seul le code unsafe est correct demande beaucoup moins d’efforts que de prouver tout le code Rust. C’est une réponse à la critique qu’on entend souvent au sujet des garanties de sûreté de Rust : « et le code unsafe, alors ? ». Les lacunes que le système de types de Rust n’est pas assez puissant pour traiter peuvent être comblées par un système plus fort comme Coq.

  • Il y a une partie que je ne comprends pas bien dans ce genre de tentative. S’il faut convertir le code en Coq manuellement ou semi-manuellement, le risque d’erreur dans ce processus n’est-il pas bien plus grand que le bénéfice apporté par la vérification formelle ?
    Autrement dit, comment savoir que ce que nous avons prouvé reste valable pour le code d’origine ?

    • On ne peut pas le savoir. Au bout du compte, il faut faire confiance à quelque chose : le matériel, le compilateur, la spécification, le noyau de confiance de Coq, etc.
      La vérification formelle est souvent présentée comme si elle éliminait totalement la possibilité de bugs, mais en pratique elle consiste plutôt à la réduire fortement. Cela dit, une traduction automatique entre Rust et Coq réduit beaucoup la complexité de ce à quoi il faut faire confiance, et devrait donc être préférée à une traduction manuelle.
    • C’est une vraie limite, mais pas une limite si grave
      Dans de nombreux cas, un bug de traduction rend tout simplement la preuve impossible. Quelqu’un cherche alors pourquoi la preuve ne passe pas, et finit par trouver le bug de traduction.
      Le vrai problème, c’est le cas où un bug de traduction annule exactement un bug du code d’origine. S’il n’y a pas de risque systémique, la probabilité que deux bugs s’annulent ainsi mutuellement est assez faible.
    • Le code est traduit automatiquement avec coq-of-rust. Si un problème est trouvé dans la traduction, il suffit de le corriger une fois dans l’outil coq-of-rust, et tous les résultats de traduction sont mis à jour.

  • Pour les lecteurs intéressés : j’ai soumis ce billet parce qu’il est moins directement lié aux cryptomonnaies que d’autres articles du même blog, mais on y trouve beaucoup d’articles techniquement plus intéressants.
    En particulier, les deux articles récents appliquent la même approche non pas à Rust, mais à Python.

  • Je me souviens d’un cours [1] où un fuzzer avait trouvé un bug dans un compilateur C formellement vérifié. C’était parce que la vérification formelle n’incluait pas le front-end ni le back-end.
    Je comprends aussi les questions sur le degré de confiance qu’on peut accorder à Coq lui-même ou à la traduction, et je me demande comment cela restera synchronisé avec les mises à jour de Rust, mais même une vérification formelle parfaite ne signifie pas une exactitude à 100 % de bout en bout.
    [1] https://youtu.be/Ux0YnVEaI6A

  • Je ne suis pas du tout spécialiste de la vérification formelle, mais si la bibliothèque de base de Rust est formellement vérifiée et n’utilise pas de code unsafe, est-ce que tous les programmes Rust qui utilisent cette bibliothèque formellement vérifiée obtiennent, pour la gestion mémoire, une qualité pratiquement équivalente à une vérification formelle ?

    • La sûreté de Rust n’a presque rien à voir avec les bugs.
      Rust a sa propre définition de “safe”, qu’on peut voir comme un sous-ensemble de la sûreté mémoire. Même dans du code Rust entièrement safe, il peut y avoir des data races, des interblocages, un épuisement de mémoire, sans parler des erreurs logiques.
    • Dans une certaine mesure, je pense que c’est le rêve, mais il y a beaucoup de réserves et plusieurs éléments doivent s’aligner.
      Premièrement, il faut formaliser la sémantique du Rust unsafe. Les travaux pionniers RustBelt[1] de Ralf Jung ont constitué une grande avancée, mais ce n’est pas encore complet. En particulier, la provenance des pointeurs s’avère être un élément délicat.
      Deuxièmement, dans ce cadre, il faut un modèle formel du borrow checker. Stacked borrows[2] était une bonne tentative mais comporte des défauts, et Tree borrows[3] pourrait les corriger, même si quelque chose de plus sophistiqué pourrait aussi apparaître.
      Troisièmement, il faut un modèle mémoire formel. Il concerne surtout le comportement des opérations atomiques et de la synchronisation, et il est donc très important pour des composants de la bibliothèque standard comme Arc. Il est largement admis que le modèle mémoire de Rust devrait être proche de celui de C++ et interopérable avec lui, mais il reste des problèmes comme “out of thin air” et des fonctionnalités manquantes comme seqlock. C’est l’une des raisons pour lesquelles le noyau Linux utilise encore son propre modèle.
      Quatrièmement, il faut prouver que les garanties de sûreté se composent bien. En particulier, la composition de code correct écrit en Rust unsafe avec du code Rust safe doit préserver les garanties de sûreté. Il existe jusqu’ici de bons résultats, mais cela doit être prouvé pour l’ensemble du système.
      Cinquièmement, pour que ce type de preuve soit valable pour tout le code, il faut fermer tous les bugs de solidité[1] restants dans Rust. Beaucoup de ces problèmes sont théoriques ou ne comptent vraiment que pour du code hostile[5], ce qui ralentit les progrès.
      Même une fois tout cela terminé, il ne s’agira toujours que de garanties partielles. Une énorme partie de la surface de contact avec le système repose sur du code unsafe. Si l’on ne fait que du calcul pur, peut-être, mais si l’on construit par exemple une interface graphique, il reste encore beaucoup de choses qui peuvent mal tourner.
      Il existe néanmoins une voie d’amélioration pragmatique, qui mène à une situation bien meilleure que l’état général actuel des systèmes criblés de vulnérabilités.
      [1]: https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf
      [2]: https://plv.mpi-sws.org/rustbelt/stacked-borrows/
      [3]: https://www.ralfj.de/blog/2023/06/02/tree-borrows.html
      [4]: https://github.com/rust-lang/rust/issues?q=is%3Aissue+is%3Ao...
      [5]: https://github.com/Speykious/cve-rs
    • Je ne suis pas spécialiste de Rust, mais il semble y avoir pas mal de unsafe dans le code de core. C’est compréhensible.
      https://github.com/search?q=repo%3Arust-lang%2Frust+unsafe+l...
      Je ne pense pas que l’approche Coq présentée ici puisse vérifier tous les appels unsafe.

  • Peut-on comparer en quoi cette approche diffère de Aeneas ou de RustHornBelt ? Comment les pointeurs et les emprunts mutables sont-ils traités ?

    • Je ne sais pas comment fonctionne RustHornBelt. Nous nous concentrons sur le code sûr, mais nous générons aussi une traduction des blocs unsafe « au mieux ».
      Par rapport à Aeneas, l’objectif est très similaire, puisque les deux cherchent à vérifier des programmes Rust avec un assistant de preuve interactif. Cela dit, dans coq-of-rust, on écrit à la main la version purement fonctionnelle du code qui servira de cible à la preuve, ou bien, comme c’est un travail répétitif, avec l’aide de GitHub Copilot, puis on prouve qu’elle est équivalente au résultat de la traduction automatique. Aeneas vise à générer directement la version fonctionnelle.
      Tous les pointeurs sont traités comme des pointeurs mutables, c’est-à-dire comme étant de type *. Nous n’utilisons pas les informations du borrow checker de Rust ; cela simplifie la traduction, mais on en paie le prix au moment de la preuve.
      Pour raisonner sur les pointeurs dans la preuve, nous permettons à l’utilisateur de fournir un allocateur personnalisé, conçu selon la façon dont la mémoire sera utilisée. Par exemple, si le programme utilise trois variables globales mutables, on peut représenter la mémoire comme un enregistrement à trois champs. Ces champs valent initialement None pour indiquer qu’ils ne sont pas encore alloués.
      Nous ne savons pas encore jusqu’où cette technique passera à l’échelle, mais pour l’instant au moins, elle permet d’éviter le raisonnement en logique de séparation. Nous nous attendons à ce que la plupart des programmes que nous voulons vérifier, en particulier côté applicatif, aient une discipline mémoire relativement « simple ».

  • Rédiger une spécification de vérification formelle ressemble-t-il à l’utilisation de tests fondés sur les propriétés plus complexes ? Au-delà des programmes simples, écrire des tests fondés sur les propriétés devient aussi assez difficile et chronophage.

    • C’est similaire, mais pas toujours identique. Les tests fondés sur les propriétés spécifient généralement une description des entrées au niveau de l’interface du système, d’une fonction ou d’une procédure, ou à un niveau plus élevé, puis testent que la sortie satisfait une propriété ou un ensemble de propriétés.
      Lorsqu’on fait de la vérification formelle au même niveau, cela peut sembler assez proche. Mais les outils de vérification formelle peuvent aller plus en profondeur. Par exemple, ils peuvent répondre à des questions sur l’état interne du système pendant un calcul, comme : « J’ai cet invariant de boucle ; peut-on prouver qu’il est effectivement préservé à chaque itération ? » ou « Peut-on prouver qu’aucun sous-dépassement ni dépassement ne se produit jamais dans aucun calcul intermédiaire au cours de ce calcul ? »
      Le premier cas est aussi possible avec des tests fondés sur les propriétés, en extrayant le cœur de la boucle dans une procédure séparée et en l’exécutant sur de nombreux états intermédiaires pour tester la propriété d’invariant. Le second est beaucoup plus difficile, sauf à découper le programme de façon extrême jusqu’à rendre chaque ligne exécutable séparément.

  • Je ne savais même pas que ce genre de chose était possible.
    Je me demande si ce type d’initiative pourrait accélérer l’adoption de Rust dans des parties centrales de son introduction dans le noyau.

  • Quelqu’un pourrait-il expliquer très simplement le concept de « vérification » ? Je me demande pourquoi un langage entier comme Coq existe uniquement pour cet objectif, et quel sens concret cela peut avoir pour la société au sens large.