Rust: au delà des types

Apporter la vérification déductive à Rust

Ce billet sera différent des autres, puisque je vais présenter ici quelques uns des premiers résultats de mon travail en tant que doctorant dans l’équipe Prosecco à l’Inria Paris, sous la supervision de Karthikeyan Bhargavan et Jonathan Protzenko. En effet, mon sujet de thèse est d’apporter à Rust le pouvoir des techniques de vérification déductive afin d’augmenter le niveau de confiance que l’on puisse avoir à propos de la correction de ses programmes. Je suis en mesure de vous présenter maintenant deux études de cas prises dans la base de code de Servo, et qui montrent à quoi peut ressembler l’utilisation de techniques de vérification.

Comment savoir qu’un programme est correct?

Premièrement, il nous faut déterminer ce que cela veut dire pour un programme d’être correct. La plupart du temps, un programme est testé sur d’un ensemble d’entrées vis-à-vis de sorties attendues. À chaque sortie du programme égale à la sortie attendue, on peut être un peu plus confiant en la correction de son programme. Mais comment être sûr que le programme va se comporter correctement dans toutes les situations? Et si nos différents cas de test avaient manqué un cas limite de notre algorithme?

Une manière d’augmenter le niveau de confiance est de tester le programme de manière systématique, par exemple grâce aux techniques de tests unitaires ou de mesure de la couverture du code. Supposons que l’on veuille tester la fonction :

fn foo(x: i32, y:i32) -> i32 {
  ...
}

Pour écrire des tests unitaires, il faut écrire des tests pour chaque sous-fonction utilisée dans foo. Avoir une couverture de code de 100% sur foo signifie que les tests explorent toutes les branches du code de foo: si foo contient une conditionnelle portant sur le test x + y > 1, il nous faut donc au moins un test où x + y > 1 et un autre où x + y <= 1. Mais même une couverture de code de 100% ne garantit pas que nos tests atteignent tous les états du programmes contenant des bugs; par exemple, les bugs d’overflow arithmétique ne sont pas automatiquement détectés par le test par couverture de code.

Tester un programme de manière systématique est chronophage, et requiert de la part du développeur la création d’un modèle mental expliquant comment le programme devrait marcher afin de créer les cas de tests les plus pertinents possibles. À l’issue de l’écriture des tests, on a deux résultats corrélés :

  1. Le développeur a réfléchi au comportement de son programme pour toutes les combinaisons des valeurs des variables d’entrées;
  2. Le niveau de confiance à propos de la correction du code est assez élevé pour un passage en production.

Cependant, ces méthodes de tests ne peuvent pas dire si vous avez manqué quelque chose. Même si le code est testé de manière minutieuse contre une certaine catégorie de bugs, il est toujours théoriquement possible qu’un bug de cette catégorie reste caché quelque part.

Les types comme outils de vérification

À POPL19, Mark Harman a présenté Sapiens, un outil d’analyse extrêmement sophistiqué qui détecte et corrige automatiquement les bugs de la base de code de Facebook. Néanmoins, il admet pendant la présentation que la puissance des analyses statiques et de l’apprentissage statistique utilisés dans Sapiens n’avaient pour l’instant été employées presque exclusivement qu’à la détection de bugs liés à des pointeurs nuls.

Pourquoi cette catégorie de bugs n’existe pas dans les programmes Rust? Tout simplement, parce qu’il est par construction impossible d’écrire et compiler un programme qui contient un bug lié à un pointeur nul. En effet, le type Option force le développeur à déclarer quelles variables peuvent prendre la valeur None, et lesquelles ne peuvent pas. En obligeant le développeur penser à cela avant l’exécution du programme, le compilateur Rust encourage à réfléchir à ce qui se passe pour les valeurs None pour toutes les combinaisons des variables d’entrée. Grâce à ce mécanisme, plus besoin de se préoccuper des bugs liés au pointeurs nuls lors du débogage.

Ce qu’il faut retenir ici est que le système de types, en rejetant à la compilation des programmes susceptibles de contenir des bugs, peut tuer dans l’œuf des catégories entières de bugs, permettant en ce faisant au développeur d’allouer plus de temps au test de propriétés plus intéressantes à propos du programme. La spécificité du système de type de Rust est qu’il est capable de garantir la sûreté mémoire des programmes ainsi que l’absence de situation de compétition, deux catégories de bugs redoutées et notoirement difficiles à débusquer en C ou C++.

Mais comment l’algorithme de vérification des types peut-il être si sûr que ce qu’il avance est vrai quelques soient les entrées? Prenons un autre exemple basé sur le type Option:

fn bar(x: Option<i32>, y:Option<i32>) -> i32 {
  match (x,y) {
      (Some(x), None) => x,
      (Some(x), Some(y)) => x + y,
      (None, None) => 0
  }
}

Vous avez déjà peut-être remarqué que ce programme est incorrect; en effet, voici l’erreur signalée par le compilateur Rust:

error[E0004]: non-exhaustive patterns: `(None, Some(_))` not covered
 --> src/main.rs:5:9
  |
2 |   match (x,y) {
  |         ^^^^^ pattern `(None, Some(_))` not covered

Comment le compilateur peut-il savoir que vous aviez oublié ce cas? En fait, le compilateur essaye de prouver que pour tous les x et y de type Option<i32>, la fonction bar va retourner une valeur de type i32. Comment prouverions-nous une telle propriété dans un cadre mathématique? Simplement en considérant tous les cas associés à Option : soit Some, soit None. Deux cas pour deux valeurs donc 4 cas au total; le match n’en a que 3 donc il nous en manque un.

Cet exemple montre une correspondance entre le code et des concepts mathématiques, et cette idée appelée la correspondance de Curry-Howard est la fondation de la recherche moderne en langages de programmation. Le but de cette branche de l’informatique est de se débarrasser systématiquement de plus en plus de catégories de bugs en prouvant leur absence des programmes, et de permettre aux développeurs de spécifier la correction de leurs programmes à l’aide de théories mathématiques de plus en plus expressives.

Un plan pour amener la vérification à Rust

Il y a de multiples de manières de produire un logiciel vérifié totalement ou partiellement. De nombreuses techniques éprouvées impliquent d’écrire le programme dans un langage haut-niveau dit de spécification, pour lequel on connaît le comportement exact de chaque construction du langage. Cependant, Rust n’a pas été conçu à cet usage et ne possède pas de formalisation complète et officielle. Le projet Rustbelt a brillamment commencé à pallier à ce problème en prouvant que les parties unsafe de la librairie standard de Rust ne mettent pas en danger les propriétés dont jouit le code safe utilisant la librairie standard.

Plus récemment, l’équipe du framework de vérification Viper a développé une interface pour Rust qui permet la vérification automatique de la sûreté mémoire et de quelques propriétés arithmétiques. En interne, Viper utilise une technique de vérification appelée exécution symbolique qui construit ses preuves sans aucune indiquation de la part de l’utilisateur. Viper utilise aussi une autre technique de vérification avec laquelle j’expérimenterai durant mon doctorat, la vérification dite déductive. Dans ce cadre, chaque fonction d’un programme possède une précondition (ensemble de choses vraies avant l’appel de la fonction) et une postcondition (ensemble de choses vraies à la sortie de la fonction). La vérification consiste à prouver que le corps de la fonction rend la postcondition vraie sous l’hypothèse que la précondition est vraie.

Comment spécifier ces préconditions et postconditions en Rust? La syntaxe et les détails sont en cours de discussion, mais cela pourrait ressembler à ça :

struct Point {
  x: i32,
  y: i32
}

fn is_diagonal(p: &Point) -> bool {
  p.x == p.y
}

#[requires="is_diagonal(p)"]
#[ensures="is_diagonal(new_p)"]
fn double(p: Point) -> new_p: Point {
    Point {
      x: p.x + p.x,
      y: 2 * p.y
    }
}

La fonction is_diagonal est la spécification de la fonction double, et n’est pas destinée à être exécutée. Elle sert plutôt de description mathématique à la fonction. Mais comment prouver cette postcondition? Ici, cela revient simplement à prouver que 2 * p.y == p.x + p.x sous l’hypothèse que p.x == p.y. Plutôt que de construire un framework de vérification ad hoc pour Rust, j’ai l’intention d’utiliser F*, un assistant de preuve semi-automatique basé sur la vérification déductive et qui utilise le prouveur automatique Z3 pour alléger la charge de preuve de l’utilisateur.

Puisque le compilateur de Rust est très puissant et les propriétés qu’il garantit déjà partiellement vérifiées grâce à des projets comme Rustbelt, je vais plutôt me consacrer à la vérification de propriétés qui ne sont pas capturées par le système de types de Rust. Plus spécifiquement, des propriétés de correction fonctionnelle comme la correction arithmétique, la validité des accès aux tableaux, la correction de machines à états, la correction fonctionnelle vis-à-vis d’une spécification abstraite, ou bien des propriétés relatives à la sécurité. Le travail principal de ma thèse sera la production d’un outil, Rox*, probablement intégré d’une manière ou d’une autre au compilateur Rust, qui traduira des programmes Rust vers du code F* qui pourra ensuite être vérifié automatiquement, ou bien à l’aide d’annotations supplémentaires de l’utilisateur.

Rust est très expressif et sophistiqué, aussi je me concentrerai sur un sous-ensemble raisonnable du langage assez expressif pour que les programmes qu’il contienne soient intéressants à vérifier. Ce sous-ensemble sera probablement construit autour d’Oxide, une nouvelle formalisation qui se focalise sur du code safe non-concurrent utilisant un nombre limité de primitives de la librairie standard. Jusqu’à présent, j’ai réalisé deux études de cas qui montrent comment mon travail pourra augmenter le niveau de confiance concernant la correction de programmes Rust réalistes.

Études de cas : TextInput et filtre de Bloom

Les deux études de cas proviennent du projet Servo, un nouveau moteur de navigateur Internet écrit en Rust et sponsorisé par Mozilla. Elles sont disponibles ici. Dans chaque cas, j’ai identifié un morceau de code qui pourrait bénéficier de vérification, puis je l’ai traduit manuellement vers un programme F* fonctionnellement équivalent et ai prouvé des propriétés sur le code F* qui augmentent notre niveau de confiance sur le code Rust. Cette traduction sera par la suite automatisée, mais ces études de cas me permettent d’évaluer la pertinence de mon approche avant de commencer le travail de développement du compilateur.

Ces deux études de cas sont présentées dans des billets séparés ici et .

Conclusion et perspectives

Ces deux études de cas m’ont aidé à identifier comment la vérification pouvait être appliquée à des programmes Rust réalistes. Certaines propriétés pourraient être spécifiées légèrement directement en Rust puis prouvées automatiquement, tandis que d’autres nécessiteront une plus grande connaissance d’un assistant de preuve comme F*. Tous les programmes n’ont pas besoin d’un niveau de confiance aussi élevé que celui offert par la vérification, et la plupart du temps le test systématique suffit. Cependant, la vérification peut parfois être plus rapide que le test systématique, et offrir une garantie formelle que le test ne pourra jamais. L’avantage est que cette méthode est également incrémentale : vous pouvez partir d’un programme qui passe le compilateur Rust, et ensuite prouver une propriété ou un invariant à la fois.

Chaque technique de vérification (exécution symbolique, vérification déductive) a ses avantages et ses inconvénients qui dépendent de ce que vous voulez prouver. Aussi est-il important qu’un futur plugin Rust pour la vérification puisse permettre de cibler plusieurs frameworks de vérification. J’ai l’intention d’utiliser Oxide comme un langage intermédiaire sémantiquement bien défini et accessible depuis le Rust HIR, afin d’en faire une plateforme commune à de futures traductions.

Le but de mon travail n’est pas fondationel, dans le sens où je n’essaie pas de prouver la sûreté ou la correction du système de types de Rust. Je ne compte pas dans un premier temps m’attaquer au difficile problème de l’interaction entre code Rust safe et code unsafe; Rustbelt est la bonne manière de le faire. Mon travail de doctorat se concentrera plutôt sur ce qui se passe au delà de la vérification de types afin d’offrir une vérification graduelle de propriétés de haut-niveau sur du code Rust, comme les études de cas le montrent.

Le mariage entre Rust et méthodes formelles a attiré l’attention d’un certain nombre de chercheurs et d’entreprises réunies dans le groupe méthodes formelles de Rust. J’espère que mon travail aidera la communauté Rust à devenir plus familière des techniques de vérification, et de la manière dont elles peuvent être utilisées afin d’augmenter le niveau de confiance en la correction de divers programmes Rust.