Benoît Boyer

Après un Post-Doc dans l'équipe DCS à VERIMAG sur la génération d'invariants linéaires d'interactions, je travaille activement depuis Juin 2012 avec Axel Legay dans l'équipe Triskell sur le développement d'un outil vérification statistique Plasma-Lab. Les algorithmes mis en oeuvre dans l'outil sont utilisés dans différents domaines tels la Bio-Chimie, la vérification de porgrammes, et plus récemment dans la vérification de systèmes complexes et hétérogènes tels que les Systèmes de systèmes. Plus d'infos sur la page de Plasma-Lab.
Auparavant, j'ai soutenu ma thèse en décembre 2010 que j'ai effectué sous la direction de Thomas Genet et de Thomas Jensen J'ai assumé la charge d'ATER à l'IFSIC / Université Rennes 1 pendant l'année 2009-2010, alors que j'effectuis mes travaux de recherche dans l'équipe Celtique à l'IRISA. Mes travaux de recherche font partie du projet RAVAJ(2006-2010). L'objectif ce projet est d'utiliser et d'étendre les techniques de vérification et d'analyses statiques basées sur la réécriture et les automates d'arbres pour analyser des programmes Java.

Mes travaux sont motivés par la vérification de programmes. En particulier, je m'intéresse à la vérification de propriétés de systèmes, pour lesquels l'ensemble des états accessibles ne peut être modélisé que de manière infinie [BW-CAV98]. Mais l'approche envisagée fonctionne aussi très bien dans le cas de systèmes à ensemble fini d’états. Il s'agit de la vérification de modèles à base de langage régulier de termes plus communément appelée Tree Regular Model Checking (TRMC) [ALRO-TACAS05]. C'est une extension de la méthode qui fut initialement introduite pour calculer l'ensemble des états atteignables en utilisant les langages réguliers de mots [BJNT-CAV00, BLW-CAV03]. En TRMC, on modélise un système de transitions (tel qu'un programme ou un protocole) par un triplet (F, I, Rel), avec:

• F une signature permettant de construire T(F) l'ensemble des termes représentants les différentes configurations ou états du système;
• I ⊆ T(F) un ensemble régulier de configurations donc représentable par un automate d'arbres A, i.e. L(A) = I;
• Rel est une relation de transition représentée par R un ensemble de règles de réécriture. Le système de réécriture doit être linéaire à gauche.

Dans ce contexte, un programme sera alors représenté par un triplet (F, A, R). Ce type de modélisation est très expressif, puisqu'il est utilisé pour modéliser des protocoles cryptographiques [AVISPA], ainsi que pour exprimer un sous-ensemble très conséquent du ByteCode Java [BGJL-RTA07]. Pour ce modèle, on considère le problème d'atteignabilité que l'on formule par la question où Bad dénote les configurations/états invalides du systèmes. Pour calculer R^*(I) l'ensemble des termes atteignables, il est possible d'utiliser la complétion d'automates d'arbres. C'est un semi-algorithme [Genet-RTA98, FGVTT-JAR04] qui calcule un automate d'arbres, i.e. une représentation régulière (et donc finie) des ensembles infinis, qui est en général une sur-approximation de R^*(I). En effet, dans les cas où R^*(I) n'est pas calculable, il est nécessaire d'accélérer l'exploration de l'espace d'états afin d'atteindre notamment les termes situés à une distance infinie des termes initiaux, pour se ramener à un temps de calcul raisonnable, ce qui revient à construire une abstraction du modèle. Ainsi, la perte d'information engendrée à l'abstraction rend le calcul possible mais moins précis: dans ce cas, on calcule une sur-approximation de l'ensemble R^*(I). En général, l'approximation est différente pour chaque problème d'atteignabilité considéré, mais l'abstraction peut être facilement exprimée au moyen d'un ensemble d'équations [MPMO-CADE03].

D'un point de vue Model Checking, la technique de vérification présentée ci-dessus n'est pas complètement satisfaisante si l'on considère le cas où la vérification échoue. En effet, il est toujours intéressant de savoir lorsqu'une configuration viole la propriété, si cela est le résultat d'une approximation trop grossière (fausse alarme) ou si le système viole réellement la propriété (contre-exemple). Dans l'état, l'algorithme permet pas cette distinction. Certains travaux se sont déjà intéressés à la question, et proposent une approche à la CEGAR (CounterExample-Guided Abstraction Refinement), c'est à dire qu'ils retirent les fausses alarmes détectées lors du calcul l'approximation. Mais ces méthodes reposent sur la construction d'un historique des différents automates obtenus à chaque étape de complétion ainsi qu'une méthode de calcul en arrière afin de déterminer si on est dans le cas d'une fausse alarme ou d'un contre-exemple.

En collaboration avec Axel Legay et Yohan Boichut, j'ai proposé une nouvelle approche basée sur des automates d'arbres instrumentés par des formules logiques et dont la sémantique permet de différencier une configuration issue de l'approximation d'une configuration atteignable. Ces automates contiennent toute l'information nécessaire pour être élagué facilement en cas d'approximation trop grossière. Pour de tels automates, nous fournissons également une procédure de test de la vacuité de l'intersection avec un automate caractérisant la propriété (les configurations interdites). Cette procédure produit une formule logique permettant de caractériser la présence d'un contre-exemple ou l'information nécessaire au raffinement l'automate.

Dans sa version originale, la complétion d'automates d'arbres permet de vérifier des propriétés de sécurité par non-atteignabilité. Il m'a semblé nécessaire d'utiliser une approche similaire pour élargir le champs des propriétés vérifiables sur les systèmes de réécriture. Ces travaux s'appliquent à étendre la complétion pour produire des automates d'arbres sur lesquels il est possible de vérifier des propriétés exprimées dans une logique dérivée de la logique temporelle linéaire (LTL), où les prédicats sont définis au moyen des automates d'arbres.

Cela m'a amené à proposer une nouvelle version de la complétion qui produit un automate d'arbres plus précis : l'introduction des ε-transitions dotées d'une sémantique bien particulière permet de donner une relation d'ordre sur les termes reconnus par l'automate. Cette relation d'ordre est en fait une abstraction de la relation de réécriture. L'ensemble des transitions silencieuses forme alors un graphe orienté dont chaque noeud dénote un ensemble de termes mis en relation par des arcs décrivant la relation abstraite de réécriture. Ce graphe est ensuite extrait de l'automate pour former une structure de Kripke décrivant sous forme de graphe la relation abstraite de réécriture. C'est en fait sur cette relation abstraite qu'il est possible de vérifier des propriétés temporelles en se rapprochant du cadre standard du Model Checking et plus précisément, des techniques de vérification basées sur des automates de Büchi.

Le problème posé est celui de la certification des résultats sous forme d'automates produits par la complétion. De tels automates sont obtenus grâce à des algorithmes complexes dont l'implantation peut contenir des erreurs. Or, la certification de la complétion, même si elle est possible, n'offre que peu d'intérêt dans la mesure où les algorithmes et implantations sont en perpétuelle évolution pour des questions de performances. Cela obligerait à reprendre la certification devenue obsolète à chaque nouvelle version de l'implantation. En revanche, un outil certifiant l'automate est plus simple et surtout plus stable dans le temps. Dans ce contexte certifier un automate résultant de la complétion consiste à montrer que ce dernier est clos par réécriture. On dit qu'un automate est clos par réécriture si les termes obtenus par réécriture des termes reconnus par l'automate sont eux-mêmes reconnus par cet automate.

Pour vérifier la propriété de clôture, j'ai défini un vérificateur d'automates d'arbre. A partir d'une description formelle de la théorie des automates et de la réécriture, j'ai prouvé que la clôture par réécriture d'un automate d'arbre est décidable. La validité de cette preuve est assurée par l'assistant de preuves Coq dans lequel la théorie est énoncée et les preuves associées sont vérifiées. Cet assistant de preuve est fondé sur la logique du calcul des constructions inductives (CCI), dont l'une des propriétés fondamentales est l'isomorphisme de Curry-Howard établissant un lien très fort entre preuve et programme. De ce lien découle le mécanisme d'extraction qui permet à partir d'une preuve d'une propriété d'extraire un programme dont l'exécution vérifie la propriété démontrée. Ainsi à partir de la preuve Coq de la décidabilité de la clôture d'un automate pour un système de réécriture j'ai extrait un programme Caml permettant de vérifier si un automate est clos par réécriture.

En contrepartie, l'isomorphisme de Curry-Horward relie fortement l'efficacité du programme et la complexité de la preuve. D'une preuve simple résulte souvent l'extraction d'un programme naïf d'une complexité médiocre. Cela m'a obligé à porter une attention toute particulière à la qualité des preuves et à la modélisation utilisée notamment pour la représentation des automates d'arbres, afin d'obtenir un vérifieur certifié et efficace.