Programmez en toute sécurité en Rust avec l’assistant de preuve Why3

Kourou. 4 juin 1996. Premier vol de la fusée Ariane 5. Trente-six secondes après l'allumage, dans le calculateur de la centrale inertielle, une valeur numérique dépasse l’espace mémoire attribué pour son stockage. Un petit bug que nul n'avait remarqué durant le développement. Privé d’information, l’auto-pilote se met en panne. La fusée quitte sa trajectoire, entraînant l’auto-destruction.

Cet accident emblématique illustre à quel point une infime erreur dans un logiciel critique peut conduire à la catastrophe. Aujourd’hui, dans un monde totalement numérisé, ces logiciels critiques régissent des pans entiers d’activités humaines. Ils régulent la circulation des trains. Régentent les transactions sécurisées. Activent les machines des blocs opératoires. Administrent les réseaux téléphoniques. Supervisent les centrales nucléaires.

Pas question donc de laisser passer le moindre bug. Mais la tâche est ardue. En 1996, il avait fallu trois ans à 16 ingénieurs pour vérifier les 90 000 lignes de code du logiciel pilotant une ligne automatique du métro parisien. De nos jours, ce travail “à la main” ne semble plus guère faisable. Car au fil du temps, les programmes sont devenus plus sophistiqués, plus complexes, plus volumineux. Impossible pour un développeur de vérifier une à une les millions de lignes de code.

D’où le besoin d’outils pour automatiser cette tâche. On les appelle des assistants de preuve. Ils reposent sur une branche des mathématiques désignée sous le terme de méthodes formelles. Au niveau international, Inria en a été un précurseur. Il y a d’abord eu le succès de Coq. Utilisé dans le monde entier et doté de fortes fondations théoriques, c’est un outil très puissant pour exprimer des complexités mathématiques. Mais il requiert de l’expertise et le développeur doit diriger lui-même le travail, étape par étape.

Why3 : preuve de programmes automatisée

Puis un autre outil a fait son apparition : Why3. Conçue par des chercheurs de Toccata, une équipe commune du centre Inria de Saclay, de l’Université Paris-Saclay et du CNRS au sein du Laboratoire des méthodes formelles (LMF) et avec le concours du CEA-List, cette plate-forme s’adresse moins aux mathématiciens qu’aux industriels. Elle permet d’effectuer de la preuve de programmes de façon automatisée, rapide et simple. À la clé pour les entreprises : une baisse des coûts. Car la vérification engloutit souvent de gros budgets.

Des tierces parties peuvent également s’appuyer sur la plate-forme pour faire fonctionner d’autres logiciels servant à vérifier des programmes écrits dans certains langages. C’est le cas, par exemple, de l’entreprise Adacore. Son application Spark se branche sur Why3 pour vérifier les programmes écrit en Ada, un langage très prisé dans l’aéronautique. De la même façon, le laboratoire List du CEA a créé Frama-C, une application qui utilise Why3 pour vérifier les programmes écrits en C.

Creusot vérifie les programmes écrits en Rust

Dans cet écosystème, un nouveau logiciel vient d’apparaître : Creusot. Conçu par Xavier Denis dans le cadre de sa thèse de doctorat au sein de Toccata co-dirigée par Claude Marché (Inria) et Jacques-Henri Jourdan (CNRS), il se branche lui-aussi sur Why3. Mais cette fois-ci, pour vérifier des programmes écrits en Rust. Ce qui en fait un utilitaire très stratégique susceptible d’intéresser beaucoup d’entreprises utilisant ce langage désormais privilégié pour le développement de logiciels critiques.

Au cœur du sujet : la gestion de la mémoire. Un point clé dans la fiabilité des programmes. “Sur les applications écrites en C, 70% des failles de sécurité résultent d’un bug de mémoire selon une étude de Microsoft, explique Xavier Denis. Ce langage date des années 1970. Il ne fournit pas de moyens pour créer un nouvel espace mémoire afin d’y stocker, par exemple, un tableau ou une structure quelconque. C’est au développeur de gérer. À lui de déterminer combien il alloue à telle chose. Or, c’est une tâche pour laquelle l’être humain s’avère assez mauvais. Il n’y arrive tout simplement pas. Au début, cela semble facile. On alloue de la mémoire. Et plus tard on la libère. Parfois, on ne s’en rend pas compte, mais on essaye d’accéder à de la mémoire que l’on a déjà libérée. Or, elle contient maintenant quelque chose d’autre. On accède ainsi à des informations auxquelles on ne devrait pas. Un mot de passe utilisateur par exemple.” Certes, des outils existent pour limiter le problème. Mais ils amoindrissent sévèrement la performance du système.

Apparu vers 2015 et porté par la Fondation Mozilla, “Rust veut combiner le meilleur des deux mondes : éviter les bugs de sécurité comme dans C sans devoir payer de surcoût pour la gestion de la mémoire. Ce langage est structuré de manière à interdire les bugs de mémoire qui lui sont présentés grâce à son système de types. Il sait quand il peut allouer de la mémoire ou quand il peut la relâcher. Et il vérifie cela à chaque fois que le programmeur lui demande de produire un exécutable.” Le tout sans ralentissement. Ce qui explique son succès. “Aujourd’hui, Rust est adopté par des grandes entreprises comme Amazon, Facebook, Google ou Microsoft.” On le retrouve aussi bien dans le navigateur Firefox que dans le système d’exploitation Android. Et bien sûr dans le monde de la cybersécurité.

Mais si ce langage possède de bonnes propriétés, les programmes ne sont pas pour autant exempts de risques. Creusot vient donc vérifier leur correction en introduisant pour ce faire deux mécanismes novateurs. Ces recherches ont donné lieu à une publication en octobre 2022.

Le programme conserve sa performance

Le premier utilisateur du nouvel outil est un étudiant de master. “Il vient d’écrire en Rust un solver de formules booléennes et l’a ensuite vérifié à l’aide de Creusot. Son solver vérifié s’avère pratiquement aussi performant que les solvers non vérifiés. Ce qui montre que l’on peut conserver la performance sans devoir faire de compromis.” 

Les travaux scientifiques, eux, se poursuivent. “Il y a des propriétés de Rust que l’on ne sait pas encore gérer. Cela serait bien d’y parvenir. C’est une grosse direction de recherche. Une nouvelle thèse de doctorat commence d’ailleurs sur le sujet.” Quant à Xavier Denis, il s’intéresse de plus en plus à l’expérience l’utilisateur. “Il y a des milliers de détails à régler pour passer d’un prototype de recherche à un outil tourné vers un usage industriel.” Un travail d’autant plus important que certaines entreprises téléchargent déjà Creusot pour commencer à l’essayer...