Expérience de recherche

Cette page est consacrée à la description de mes travaux de recherche effectués successivement dans les équipes PROTHEO, CASSIS puis Pesto du LORIA (Laboratoire Lorrain de Recherche en Informatique et ses Applications). Je commence par décrire les principaux résultats obtenus pendant ma thèse, puis ceux obtenus plus récemment. Je présente ensuite la liste de mes activités annexes (administratives et scientifiques).
Ces présentations de mes activités de recherche font référence à la liste de publications.

Voici auparavant une petite introduction sur les principaux thèmes de recherche auxquels je m'intéresse.

Déduction automatique

La démonstration automatique est née historiquement de la tentative de mécanisation des mathématiques, et donc d'automatiser la production de théorèmes. Les premiers travaux issus de la découverte par Alan Robinson du principe de la résolution sont à la base des concepts et des outils de la programmation logique, devenue aujourd'hui l'un des principaux paradigmes programmatoires. Les années 80 ont consacré l'automatisation du raisonnement équationnel, permettant la manipulation mécanique des spécifications algébriques.

Dans la continuité de cette évolution, je me suis intéressé à la recherche de stratégies complètes efficaces de démonstration automatique en logique du premier ordre, et plus particulièrement à des stratégies de déduction dans des théories exprimées par un ensemble d'équations. Les applications essentielles concernent les systèmes experts, la vérification de programmes, et la performance dans la preuve de théorèmes.

Déduction avec contraintes

Les contraintes se sont révélées un outil puissant aussi bien pour la modélisation du processus de déduction que pour l'optimisation des procédures de base comme l'unification. Mes travaux dans ce domaine portent sur la définition de stratégies contraintes pour la déduction automatique dans une théorie.

Techniques de normalisation

Les techniques de réécriture ont été appliquées avec succès à de nombreux domaines de l'informatique et des mathématiques. Mentionnons pour mémoire : la conception et l'implantation des langages fonctionnels, l'analyse et l'implantation des spécifications algébriques de types abstraits, la construction de systèmes de démonstration automatique efficaces, la construction de systèmes de calcul symbolique. La théorie de la réécriture est une théorie des formes normales. Ainsi le raisonnement équationnel nécessaire pour démontrer une égalité A=B peut se réduire sous certaines hypothèses à la comparaison des formes normales de A et B. L'évaluation en programmation fonctionnelle s'interprète également comme un calcul des formes normales. Le modèle initial d'une spécification correspond le plus souvent au modèle d'intérêt du programmeur. Or, ce modèle se décrit naturellement par un ensemble de formes normales closes lorsque la spécification se présente comme un système de réécriture.

Les algorithmes de normalisation sont donc cruciaux pour des applications comme la vérification automatique et la programmation fonctionnelle. J'ai étudié de nouvelles méthodes qui pourront être mises au point dans le système de démonstration automatique daTac, développé pendant ma thèse.

Logiques non classiques

Le raisonnement dans des logiques faisant intervenir une notion d'incertitude peut être mécanisé de deux manières différentes : en donnant des règles de raisonnement spécifiques dans le langage "incertain", ou en traduisant les opérateurs d'incertitude au premier ordre. La tendance actuelle privilégie les traductions au premier ordre avec théories équationnelles de façon à profiter de l'efficacité des techniques de réécriture.

Je me suis intéressé à la recherche de propriétés de logiques dites "approximantes", à l'aide du système daTac.

Protocoles cryptographiques

La sécurisation des échanges d'informations sur un réseau est un problème très important de nos jours, mis en valeur par la banalisation d'Internet. Ainsi, par exemple, tout achat sur le web commence par une phase d'authentification des acteurs, c'est-à-dire de la banque, du vendeur et de l'acheteur, afin que chacun soit sûr de ses interlocuteurs. Cette phase se déroule en suivant un protocole prédéfini.

De nombreux protocoles ont été mis au point, mais il s'avère qu'un grand nombre d'entre eux ne sont pas sûrs à 100%. Certains permettent à un intrus, par exemple, de récupérer des informations confidentielles, de se faire passer pour quelqu'un d'autre, ou de perturber un échange d'informations.

Dans ce domaine, je participe au développement de méthodes et d'outils permettant de simuler des protocoles pour essayer de trouver leurs failles. Je m'intéresse également à la définition de techniques permettant de montrer qu'un protocole est sûr.

* * * Résultats obtenus pendant la thèse * * *

La déduction automatique est de plus en plus souvent utilisée dans de nombreux domaines (calcul formel, validation de programmes, programmation logique, etc.). Mais, les techniques classiques de déduction sont inefficaces lorsque des fonctions possèdent des propriétés pourtant aussi courantes que l'associativité et la commutativité. Il est donc fondamental de pouvoir raisonner efficacement dans la théorie engendrée par ces propriétés.

Je me suis donc penché sur la définition de techniques pour simuler une théorie, en particulier grâce à de nouvelles règles d'inférence, en gardant pour principal objectif l'efficacité. Nous avons abouti à la définition de nouvelles stratégies de preuves.

- Déduction modulo AC

Le domaine de la déduction automatique en logique du premier ordre en présence de fonctions associatives et commutatives (AC) est réputé difficile. Aussi, lors de mon DEA [Vig90], j'ai commencé par étudier l'état de l'art et je me suis aperçu que les axiomes traduisant ces propriétés étaient systématiquement ajoutés, ce qui augmentait énormément le nombre de déductions possibles. Avec M. Rusinowitch, nous avons proposé de traiter ces propriétés par des mécanismes évitant l'usage explicite de ces axiomes qui causent une explosion combinatoire et engendrent des preuves trop indirectes.

Le résultat principal a été l'élaboration d'un système de règles d'inférence. Ce système, basé sur les règles de résolution (pour des déductions entre prédicats) et de paramodulation (pour des déductions avec des équations), est compatible avec des règles d'élimination ou de simplification de clauses redondantes. Mais, la définition d'un tel système ne suffit pas ; il faut prouver qu'il est complet par réfutation, c'est-à-dire qu'il pourra toujours dériver une contradiction d'une spécification initiale incohérente. Nous avons donc montré que notre système est réfutationnellement complet en étendant aux théories AC la technique des arbres sémantiques transfinis, définie par M. Rusinowitch dans sa thèse. Ce travail a été présenté à la conférence FAIR'91 [RV91].

- Systèmes d'inférence

Ainsi, je me suis consacré à la définition de stratégies permettant de limiter le nombre d'applications des règles d'inférence. Les principales améliorations sont la restriction des étapes de paramodulation aux positions maximales des opérateurs AC, l'obligation de travailler avec l'atome maximal d'une clause, et un fort contrôle de l'application des règles d'inférence simulant l'utilisation de clauses étendues ; ces clauses sont habituellement produites par l'axiome d'associativité et sont une cause de divergence des démonstrateurs classiques.

Ces restrictions ont abouti à la définition d'un système de règles d'inférence pour la stratégie positive, qui consiste à ne permettre des déductions que si elles utilisent au moins une clause n'ayant que des éléments positifs, c'est-à-dire une clause sans conditions. Cette stratégie a été présentée au workshop CCL'92 [RV92].

- Technique de preuve de complétude

Comme je l'ai précisé auparavant, il faut démontrer que les systèmes de règles que l'on utilise sont complets. J'ai mis au point une nouvelle méthode de preuve, améliorant considérablement celle de mon DEA. Elle est beaucoup plus naturelle mais toujours fondée sur la construction d'arbres sémantiques. Elle a fait l'objet d'une publication qui est parue dans le journal AAECC [RV95].

Cette méthode, initialement définie pour le cas des théories AC, a pu facilement être adaptée pour montrer la complétude de la stratégie contrainte, et être étendue à des théories équationnelles plus générales que AC [Vig94f].

En particulier, j'ai montré que la règle de paramodulation pouvait être remplacée par la règle de superposition tout en conservant la complétude du système d'inférence [Vig94b]. La stratégie obtenue, dite stratégie de superposition, consiste à n'effectuer des remplacements que dans le plus grand membre des équations.
Des preuves de complétude de cette stratégie (dans la théorie vide) avaient déjà été réalisées avec la technique des arbres sémantiques, mais elles apportaient toutes des restrictions sur l'application de la stratégie.

- Déduction contrainte modulo AC

Je me suis également intéressé à l'intégration de contraintes dans les systèmes d'inférence définis, motivé par les problèmes suivants :

- Contraintes symboliques

La solution que j'ai adoptée pour ces problèmes a consisté à manipuler des contraintes symboliques, c'est-à-dire à accumuler dans chaque clause les conditions d'application des règles d'inférence sous forme de contraintes qui en quelque sorte conservent une trace des déductions qui ont abouti à cette clause. Ainsi, nous avons des contraintes d'ordre qui permettent d'avoir une trace de tous les choix effectués, et des contraintes d'unification rassemblant les problèmes d'unification AC rencontrés.

Le but visé est de ne plus calculer les solutions d'un problème d'unification, mais de vérifier simplement qu'il en existe au moins une. Ces contraintes permettent de représenter très naturellement la stratégie basique, qui consiste à interdire toute déduction dans un terme introduit lors d'une étape d'inférence précédente, c'est-à-dire dans un terme importé par l'instanciation d'une variable. En effet, les unificateurs n'étant plus calculés, les variables ne sont plus instanciées. Une première version de ce travail a été présentée au workshop CCL'93 [Vig93].

- Élimination de l'unification

Cependant, le système de règles d'inférence décrit lors de cet exposé comportait encore quelques résolutions de problèmes d'unification, pour conserver la complétude du système.
En modifiant certaines conditions d'application de règles d'inférence, j'ai réussi à éviter ces résolutions. Ce résultat a été présenté à la conférence CADE'94 [Vig94d]. La preuve de complétude réfutationnelle de ce système avec contraintes symboliques est une adaptation très simple de la preuve sans contraintes.
Ces contraintes sont également compatibles avec la stratégie de superposition.

Une conséquence de ces résultats est que la stratégie basique, consistant à résoudre les problèmes d'unification mais à ne pas appliquer les solutions dans les clauses déduites, est également complète.

Un cadre général de déduction avec contraintes, détaillant les nouveaux centres d'intérêt soulevés, a été présenté avec H. Kirchner au workshop Theory Reasoning in Automated Deduction de cette conférence CADE'94 [KV94].

- Implantation : daTac

Tous ces résultats concernant la déduction dans des théories AC ont été implantés au fur et à mesure dans un logiciel nommé daTac (Déduction Automatique dans des Théories Associatives et Commutatives). La programmation a été réalisée en CAML Light, un langage fonctionnel de la famille ML, développé à l'INRIA Rocquencourt. Le logiciel conçu est un démonstrateur de théorèmes spécialisé dans la déduction en présence de propriétés d'associativité et de commutativité. Pour cela, il utilise une procédure d'unification AC, basée sur l'algorithme de Stickel, muni de la technique de résolution des équations Diophantiennes de Fortenbacher. Il contient aussi une procédure de filtrage AC, indispensable pour détecter les clauses redondantes.

Ce logiciel n'a cessé d'évoluer. Actuellement, il met à la disposition de l'utilisateur les nombreuses stratégies de déduction décrites dans ce chapitre, y compris les stratégies basiques et contraintes. Il est constitué d'environ 20000 lignes de code, et muni d'une interface graphique écrite en Tcl/Tk. Le fait qu'il soit écrit en CAML Light le rend portable sur stations SUN, HP, PC et Macintosh.

daTac
daTac : Fenêtre principale de l'interface

daTac
daTac : Fenêtre d'exécution de l'interface

daTac a été très utile pour tester les stratégies définies, mais aussi pour mettre au point de nouvelles stratégies, comme la stratégie basique. Cette dernière est la plus efficace, la stratégie contrainte nécessitant des outils spécifiques pour traiter l'ensemble des contraintes accumulées.

- Déduction modulo E

J'ai généralisé la technique de traitement des théories associatives et commutatives à une classe beaucoup plus large de théories équationnelles, incluant l'ensemble des théories régulières (théories préservant les variables). Ce résultat, annoncé lors du workshop UNIF'94 [Vig94c], généralise les travaux existant dans ce domaine. Il comprend la définition d'un algorithme de calcul des extensions utiles des clauses [Vig96a], l'un des principaux problèmes lorsque l'on travaille dans une théorie équationnelle. Ces travaux ont été présentés à la conférence CSL'95 [Vig95b], avec en plus une nouvelle version (encore plus efficace) de la stratégie positive.

* * * Travaux "récents" * * *

Ces dernières années, je me suis toujours intéressé à la définition de techniques efficaces de déduction, mais je me suis aussi orienté vers les nombreuses applications de la déduction automatique.

- Techniques efficaces de réécriture

Au cours de mon année post-doctorale à l'Université de Stony Brook, je me suis penché avec L. Bachmair et I. V. Ramakrishnan sur les problèmes d'efficacité de la réécriture. En particulier, nous nous sommes rendus compte que dans tous les outils de déduction automatique les étapes de simplification par réécriture sont souvent répétitives. Par exemple, dans la procédure de complétion de Knuth-Bendix, les paires critiques calculées doivent être normalisées par les règles de réécriture déjà trouvées. Or, il s'avère que d'une paire critique à une autre nous retrouvons souvent les mêmes termes ou sous-termes à normaliser. D'où une perte d'efficacité considérable à répéter les mêmes calculs.

Nous avons donc mis au point une technique qui consiste à se souvenir des étapes de réécriture déjà effectuées grâce à ce que nous pourrions appeler un historique. Il ne s'agit pas de mémoriser toutes les étapes de réécriture, mais seulement d'accéder directement à la forme normale (irréductible) d'un terme donné. De plus, si un terme a plusieurs formes normales, nous n'en retenons qu'une seule.
Notre méthode est telle qu'il n'est jamais nécessaire d'appliquer deux fois la même règle de réécriture. Dès qu'une règle est appliquée, elle est propagée dans les autres termes de la base de données grâce à une représentation très efficace des termes. Et lorsqu'un terme est ajouté à la base de données, il est automatiquement normalisé pour les règles de réécriture déjà appliquées.

Nous avons étendu ce résultat pour la réécriture modulo des propriétés d'associativité et de commutativité. Cette extension est très avantageuse, car l'axiome de commutativité ne peut être orienté en une règle de réécriture.
Ces premiers résultats ont été présentés au workshop CCL'96 [BRV96].

Étant persuadés que cette nouvelle vision de l'utilisation de la réécriture est un point clé dans la recherche continuelle d'efficacité des outils de déduction automatique, nous avons mis au point une procédure très facile à implanter. L'implantation réalisée lors d'un séjour à Stony Brook en 1998, puis complétés par A. Tiwari [TV00a], permet de résoudre le problème de clôture par congruence de systèmes sans variables en des temps records. Ce travail a ensuite été étendu pour considérer des opérateurs associatifs-commutatifs, résultat présenté à la conférence FroCoS 2000 [BRTV00b]. Notre technique permet de représenter les anciennes méthodes de clôture par congruence comme des stratégies d'application de nos règles, ce qui a permis de mieux comprendre les liens entre ces différentes méthodes (article publié dans le journal JAR [BTV03]).

- Applications de la déduction automatique

Les techniques de déduction définies dans ma thèse ont été implantées dans le logiciel daTac, et ces différents algorithmes et stratégies n'ont cessé d'être améliorés. Cette efficacité toujours croissante a permis d'essayer daTac pour résoudre des problèmes réels.

- Algèbres approximantes

Je travaille avec A. Wasilewska, une logicienne de l'Université de Stony Brook, s'intéressant à la théorie des ensembles approximants (rough sets). Cette théorie concerne l'analyse de classification d'informations imprécises, incertaines ou incomplètes, ou bien de connaissances exprimées en terme de données acquises par expérience.

Nous nous sommes plus particulièrement intéressés aux théories approximantes définies à l'aide d'algèbres Booléennes ou quasi-Booléennes et d'opérateurs topologique. Ces algèbres récentes, modélisant des logiques non classiques (comme les logiques modales S4 et S5, par exemple) restent mal connues. Nous avons donc utilisé le logiciel daTac non comme un démonstrateur mais comme un générateur de théorèmes. Les premiers résultats ont été présentés lors du workshop RST'95 [WV95].
Les centaines de propriétés déduites nous ont permis de mieux comprendre ces algèbres. L'avantage considérable offert par daTac est qu'il permet de retrouver très facilement la preuve complète d'une propriété trouvée. La description des résultats obtenus ainsi que celle des stratégies utilisées pour isoler les propriétés intéressantes a été publiée dans le livre Rough Sets in Knowledge Discovery [WV98].

Pour compléter l'étude de ces algèbres, nous avons mis au point une procédure permettant de comparer plusieurs algèbres avec daTac, et l'avons appliquée à la comparaison de nos algèbres approximantes. Ces travaux ont été présentés à la conférence CESA'96 [VW96a].
Cette application à l'étude de logiques non classiques a été présentée à la communauté de déduction automatique lors du workshop CCL'96 [VW96b].

Nous nous sommes aussi penchés sur le problème de la définition d'algèbres pour les ensembles approximants. Nous avons ainsi montré que les algèbres définies par A. Wasilewska permettent non seulement de formaliser les ensembles approximants, mais en fait qu'elles les généralisent [WV97].

Nos derniers travaux ont consisté à étudier la notion de congruence dans les espaces topologiques. Nous avons montré l'existence d'une congruence sur les espaces dits clopen, l'avons construite, puis avons démontré que l'espace quotienté par cette congruence est modélisé par une algèbre topologique quasi-Booléenne. Ces preuves ont été faites avec daTac, mais elle ont d'abord été intuitées graphiquement, à l'aide de diagrammes [VW98a] [VW98b].
Nous essayons maintenant de définir une technique combinant cet aspect graphique et le démonstrateur [VW99] [WLV99].

Une description des techniques de déduction dans une théorie, ainsi que l'exemple de leur application aux logiques non classiques, ont été présentés lors de la conférence LACS'96 [Vig96c], et ont été publiés dans le journal Fundamenta Informaticae [Vig98].

- Protocoles cryptographiques

Avec M. Rusinowitch et F. Jacquemard, nous étudions des protocoles permettant à deux utilisateurs d'un réseau de s'identifier formellement dans le but de s'échanger des informations cryptées. De nombreux protocoles existent, mais récemment des trous de sécurité ont été découverts dans des protocoles largement diffusés. Et avec la popularisation d'Internet et l'importance croissante des transactions confidentielles, il est indispensable de vérifier la correction des protocoles utilisés.
S'il est relativement facile pour un expert de trouver à la main des erreurs dans de petits protocoles, il est indispensable d'utiliser des outils automatiques ou semi-automatiques pour vérifier la plupart des protocoles actuellement utilisés, comme SET pour le commerce électronique.

Nous avons proposé une sémantique opérationnelle pour les protocoles d'authentification fondée sur la surréduction associative et commutative [JRV00b] [JRV00a].

Plus précisément, nous avons conçu un logiciel (Casrul) qui compile une description standard d'un protocole en un système de réécriture qui peut ainsi servir à la simulation des exécutions du protocole à partir d'états initiaux. Cela permet d'une part de définir formellement la sémantique opérationnelle des protocoles et par exemple de vérifier qu'ils sont implantables. D'autre part, le compilateur engendrant des règles de réécriture, elles peuvent être envoyées presque telles quelles à des systèmes de preuves automatiques. Nous utilisons le démonstrateur daTac sur le résultat car il manipule une logique équationnelle bien adaptée. daTac cherche à résoudre un but qui représente l'existence d'une attaque. Nous pouvons également compiler les buts et le comportement d'un intrus dont le rôle est de perturber le déroulement du protocole.
Nous avons défini une stratégie paresseuse du comportement de l'intrus, pour une meilleure efficacité de la recherche de failles [CV01b] [CV01a].

Notre méthode, contrairement au méthodes de model-checking, n'oblige pas à fixer des bornes sur tous les paramètres qui pourraient sembler diverger pour assurer la terminaison de la vérification. Ainsi, nous avons montré que la taille des messages engendrés par l'intrus n'a pas à être bornée artificiellement [CV04].
De même, grâce à la distinction entre les participants normaux d'un protocole et ceux qui seront manipulés (contre leur volonté) par l'intrus, il n'est également pas nécessaire de borner le nombre d'exécutions du protocole [CV02a].

Les travaux récents sur ce thème se sont faits dans le cadre d'un projet européen (Information Society Technologies (IST) Programme, FET Open Assessment Project AVISS, IST-2000-26410), en collaboration avec Gênes (Italie) et Fribourg (Allemagne). Ils se poursuivent par un nouveau projet sur 3 ans (Information Society Technologies (IST) Programme, FET Open Project AVISPA, IST-2001-39252), en collaboration avec Gênes (Italie), Zurich (Suisse) et Siemens Munich (Allemagne). Une plate-forme de vérification de protocoles a déjà été élaborée [ABB+02], montrant l'efficacité incontestable de nos techniques conjointes sur un très grand nombre de protocoles, permettant par exemple de trouver une faille dans un protocole qui était jugé sûr jusque-là (Denning-Sacco).

* * * Implications administratives et scientifiques * * *

- Activités diverses