Traduction des crates `core` et `alloc` de Rust vers Coq pour une vérification formelle

Traduction des crates core et alloc de Rust

Exécution initiale 🐥

• En lançant une première exécution sur les crates alloc et core de Rust avec coq-of-rust, deux fichiers de code Coq de plusieurs centaines de milliers de lignes ont été générés.
• Cela montre que l’outil fonctionne même sur de grosses bases de code, mais le code Coq généré ne compile pas. Les erreurs sont rares (environ une toutes les quelques milliers de lignes).

Taille du code Rust en entrée (d’après la commande cloc)

• alloc : 26 299 lignes de code Rust

• core : 54 192 lignes de code Rust

• Comme la traduction doit se faire après expansion des macros, la taille réelle à traduire est encore plus importante.

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

• Le principal changement consiste à avoir découpé la sortie générée par coq-of-rust en un fichier par fichier Rust d’entrée.
• Cela est possible parce que la traduction peut se faire indépendamment de l’ordre des définitions. Les dépendances circulaires entre fichiers Rust sont interdites en Coq, mais le découpage reste possible.

Taille de la sortie

• alloc : 54 fichiers Coq, 171 783 lignes de code Coq
• core : 190 fichiers Coq, 592 065 lignes de code Coq

Avantages du découpage du code

• Le code généré est plus facile à lire et à parcourir
• La compilation est plus simple car elle peut être parallélisée
• Le débogage est plus simple en se concentrant sur un seul fichier
• Il est plus facile d’ignorer les fichiers qui ne compilent pas
• La maintenance est facilitée car il est plus simple de suivre les changements dans un fichier unique

Correction de quelques bugs 🐞

• Il y avait un bug causé par des conflits entre noms de modules. Il se produisait lors du choix du nom de module pour les blocs impl.
• Davantage d’informations ont été ajoutées aux noms de modules pour renforcer leur unicité. Par exemple, une clause where a été ajoutée.

Exemple

• Implémentation du type Mapping pour le trait Default :

  #[derive(Default)]
  struct Mapping<K, V> {
    // ...
  }
  

• Ancien code Coq :

  Module Impl_core_default_Default_for_dns_Mapping_K_V.
  (* ...trait implementation ... *)
  End Impl_core_default_Default_for_dns_Mapping_K_V.
  

• Code Coq corrigé :

  Module Impl_core_default_Default_where_core_default_Default_K_where_core_default_Default_V_for_dns_Mapping_K_V.
  (* ... *)
  

Liste des fichiers qui ne compilent pas

• 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 représente 4 % de l’ensemble des fichiers. Même dans les fichiers qui compilent, il peut subsister des structures Rust non prises en charge.

Exemple 🔎

Code source de la méthode unwrap_or_default du type Option

pub fn unwrap_or_default(self) -> T
where
  T: Default,
{
  match self {
    Some(x) => x,
    None => T::default(),
  }
}

Code Coq traduit

Definition unwrap_or_default (T : Ty.t) (τ : list Ty.t) (α : list Value.t) : M :=
  let Self : Ty.t := Self T in
  match τ, α with
  | [], [ self ] =>
    ltac:(M.monadic
      (let self := M.alloc (| self |) in
      M.read (|
        M.match_operator (|
          self,
          [
            fun γ =>
              ltac:(M.monadic
                (let γ0_0 :=
                  M.get_struct_tuple_field_or_break_match (|
                    γ,
                    "core::option::Option::Some",
                    0
                  |) in
                let x := M.copy (| γ0_0 |) in
                x));
            fun γ =>
              ltac:(M.monadic
                (M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                    []
                  |)
                |)))
          ]
        |)
      |)))
  | _, _ => M.impossible
  end.

Version simplifiée de la fonction

Definition unwrap_or_default {T : Set}
  {_ : core.simulations.default.Default.Trait T}
  (self : Self T) :
  T :=
  match self with
  | None => core.simulations.default.Default.default (Self := T)
  | Some x => x
  end.

• Cette définition simplifiée est utilisée lors de la vérification du code. La preuve d’équivalence se trouve dans CoqOfRust/core/proofs/option.v.

Conclusion

• La formalisation de la bibliothèque standard permet de rendre fiables les travaux de vérification des programmes Rust.

• L’objectif suivant est de simplifier un processus de preuve encore fastidieux. En particulier, il s’agit de séparer les étapes de résolution des noms, d’introduction de types avancés et d’élimination des effets de bord lorsqu’on montre que la simulation est équivalente au code Rust d’origine.

• Si vous êtes intéressé par la vérification formelle de projets Rust, contactez [e-mail]. La vérification formelle offre le plus haut niveau de sûreté en garantissant mathématiquement l’absence de bugs vis-à-vis d’une spécification donnée.

Tags :

• coq-of-rust
• Rust
• Coq
• traduction
• core
• alloc

L’avis de GN⁺

1. Intégration de Rust et Coq : l’intégration de Rust et Coq aide fortement à améliorer la fiabilité des programmes Rust. Combiner la sûreté de Rust et la vérification formelle de Coq est particulièrement utile pour les applications critiques.
2. Importance de l’automatisation : la traduction automatique avec l’outil coq-of-rust est plus fiable qu’un travail manuel. Il faut toutefois rester prudent, car des erreurs peuvent encore survenir pendant le processus de vérification.
3. Gestion des bases de code complexes : pour gérer de grosses bases de code, le découpage facilite grandement la maintenance et le débogage. C’est un point particulièrement important dans le travail en équipe.
4. Nécessité de la vérification formelle : la vérification formelle est indispensable dans des domaines critiques comme la finance, la santé ou l’aéronautique. L’association de Rust et Coq peut y apporter une grande valeur.
5. Points à considérer lors de l’adoption : lors de l’adoption d’une nouvelle technologie, il faut prendre en compte la courbe d’apprentissage et la compatibilité avec les systèmes existants. Des outils de vérification formelle comme Coq peuvent avoir une courbe d’apprentissage élevée et nécessitent donc une préparation et une formation suffisantes.

[GN⁺]

Commentaire Hacker News

Résumé d’une sélection de commentaires Hacker News

• Fiabilité des outils de traduction automatique

  • Les outils de traduction automatique inspirent confiance. coq-of-rust est écrit en Rust et peut être converti en Coq pour en prouver la correction. Cela ressemble à une méthode pour se prémunir contre l’attaque de Ken Thompson.

• Taille des programmes et vérification

  • La taille des programmes vérifiés avec des systèmes de preuve semi-automatiques comme Coq reste faible. Le coût d’une garantie à 100 % peut être dix fois supérieur à celui d’une garantie à 99,9999 %.

• Possibilité d’erreurs dans le processus de traduction

  • Il est probable que des erreurs surviennent lors de la traduction du code vers Coq. Cela fait douter de la validité de la vérification appliquée au code source.

• Publications liées aux cryptomonnaies

  • Un billet de blog contenant peu d’éléments liés aux cryptomonnaies a été partagé. Il existe aussi un billet traitant d’une approche similaire pour Python.

• Limites de la vérification formelle

  • Quelqu’un se souvient d’un cas où un bug avait été trouvé dans un compilateur C formellement vérifié. Cela soulève des questions de confiance envers Coq lui-même et envers la traduction.

• Vérification formelle de Rust

  • Si la bibliothèque standard de base de Rust était formellement vérifiée, on se demande s’il serait alors possible d’obtenir ce niveau de garantie pour la gestion mémoire tant qu’on n’utilise pas de code unsafe.

• Rédaction de spécifications de vérification formelle

  • On se demande si rédiger des spécifications de vérification formelle ressemble à écrire des tests de propriétés plus complexes. Écrire des tests de propriétés est difficile et prend du temps.

• Comparaison avec d’autres approches

  • Quelqu’un demande une comparaison avec des approches comme Aeneas ou RustHornBelt. Il s’interroge sur la manière dont les pointeurs et les emprunts mutables sont gérés.

• Adoption de Rust dans le noyau

  • On se demande si ce type d’effort pourrait accélérer l’adoption de Rust dans le noyau.

• Ajout d’un backend Rust à F*

  • On se demande quelle quantité de travail serait nécessaire pour ajouter un backend Rust à F*.