Xavier Rival : vérifier automatiquement la sûreté des logiciels critiques

Date:
Mis à jour le 15/10/2020
Cette année encore, quatre jeunes chercheurs d’Inria ont décroché une bourse du très sélectif Conseil européen de la recherche (ou European Research Council , ERC) pour mener pendant cinq ans une recherche exploratoire, avec un budget de 1 à 1,5 million d’euros. Xavier Rival, chercheur en informatique, membre de l’équipe-projet Abstraction, est un des lauréats. Il explique son projet.

Une erreur dans un logiciel peut avoir des conséquences humaines ou économiques catastrophiques, surtout s’il s’agit d’un logiciel critique comme ceux qui commandent des systèmes aéronautiques, aérospatiaux, nucléaires, médicaux ou automobiles. Comment être sûr que le logiciel s’exécutera systématiquement sans erreur ? C’est à cette question complexe que tente de répondre Xavier Rival. Et ce jeune trentenaire, normalien, a de quoi faire quand on sait que 99% des industriels vérifient leurs logiciels, tout simplement en testant tout ou partie de leur exécution des centaines de fois de suite… et en gageant que le résultat sera reproductible.

Dans l’équipe Abstraction, nous développons des méthodes d’analyse automatique de code qui permettent de vérifier l’ensemble des exécutions d’un programme en un seul calcul

Autrement dit, ces analyseurs calculent des preuves au sens mathématique. Outre l’intérêt économique – des logiciels de taille industrielle sont testés en une journée de calcul - le résultat est parfaitement fiable. C’est d’ailleurs suite à l’explosion d’Ariane 5, en 1996, due à une erreur logicielle, que les outils de vérification de logiciels ont commencé à conquérir le monde industriel. L’analyseur Astrée  a été conçu dans ce contexte, depuis 2001. Xavier Rival a participé à son développement dès sa thèse (École polytechnique) dans un laboratoire de l’École normale supérieure. De manière plus générale, ces dernières années, des progrès importants ont été accomplis, en particulier pour les logiciels qui effectuent des calculs numériques, comme ceux vérifiés par Astrée.

 Il reste beaucoup à faire pour les logiciels qui manipulent des structures de données complexes en mémoire (listes, arborescences, files d'attente).

« En revanche, on ne sait pas analyser aussi bien les nombreux logiciels embarqués, moins critiques, mais qui ont besoin de faire appel à des données complexes en mémoire, comme les logiciels de communication, de navigation, les protocoles d’échange de données... C’est l’objet de mon projet ERC »,  précise t-il. Cela permettrait d’élargir le domaine d’application de ces outils. Xavier Rival a eu l’occasion de se frotter à ces problématiques ardues depuis 2006 dans le cadre d’une collaboration avec Bor-Yuh Evan Chang, amorcée lors de son postdoc à Berkeley, puis lorsqu’il a rejoint l’institut en 2007. De bons algorithmes existaient pour rendre automatique l’analyse de logiciels effectuant des calculs numériques, en décomposant des propriétés logiques en éléments simples. Pourtant, il reste beaucoup à faire pour les logiciels qui manipulent des structures de données complexes en mémoire, que ce soit sous forme de listes, d’arborescence, de files d’attente… Cela rend les raisonnements et leur automatisation très compliqués. « Après avoir mûri mon idée pendant un an ou deux, je me sens prêt à relever le défi », conclut-il. Sa bourse ERC lui permettra de travailler avec trois doctorants, trois postdoc et un ingénieur pendant cinq ans, ainsi que d’inviter des professeurs pour des collaborations courtes.

"Astrée " continue de faire ses preuves

Conçu et développé dans l’équipe-projet Abstraction, cet analyseur de code est commercialisé depuis 2009 par AbsInt Angewandte Informatik, une spin-off de l’université de la Sarre (Allemagne). Il permet, via un calcul automatique, de vérifier certains logiciels critiques embarqués, écrits en langage C, tels que des commandes de vol électriques. L’approche est fondée sur l’approximation sûre, une surapproximation de l’ensemble des comportements possibles du code lors de l’exécution du logiciel qui permet de n’omettre aucune erreur mais peut en revanche générer de fausses alarmes. Le défi est de rendre cet outil relativement générique toujours plus précis pour limiter ces fausses alarmes.