Section 06 Sciences de l'information : fondements de l'informatique, calculs, algorithmes, représentations, exploitations

II. Fondements de l'informatique, preuve et vérification

L'informatique fondamentale s'attache à étudier et à systématiser les démarches, parfois empiriques, mises en œuvre dans le développement logiciel, ainsi qu'à concevoir de nouveaux cadres ou méthodologies. Cette thématique se situe à la croisée d'une variété de domaines tels que la logique, la théorie des automates, les systèmes de réécriture, les algèbres de calcul et encore des systèmes de contraintes. Les applications sont diverses, allant de la conception à l'analyse de codes sûrs (codes embarqués, systèmes répartis ou mobiles, protocoles de sécurité, ou plus généralement, tous les codes dont le bon fonctionnement est crucial d'un point de vue économique, médical ou sociétal). L'implication de la communauté française dans ces domaines de recherche est très importante avec de nombreux projets et réseaux européens.

A. Avancées majeures

Une avancée récente importante se situe au cœur de nombreux problèmes de vérification et concerne les réseaux de Petri, des objets introduits dans les années 60 pour modéliser des processus concurrents. Il s'agit du problème crucial de l'accessibilité dans ces réseaux, pour lequel le premier algorithme, très complexe tant d'un point de vue conceptuel que d'un point de vue calculatoire, n'a été proposé qu'au début des années 1980. Après de nombreuses recherches pour développer des solutions plus simples, la France a récemment eu un rôle moteur et décisif, en développant un nouvel algorithme qui repose sur une toute nouvelle approche conceptuellement simple, à savoir le calcul d'invariants inductifs presque semi-linéaires permettant de valider soit l'accessibilité, soit la non-accessibilité. Ces résultats ouvrent de nouvelles perspectives, qui permettront, peut-être dans un futur proche, de mieux cerner la complexité théorique intrinsèque du problème de l'accessibilité dans les réseaux de Petri.

Une autre avancée notable porte sur le format standard XML (eXtensible Markup Language) pour l'échange de données semi-structurées qui est utilisé dans des services web, les bases de données, et pour échanger des données entre applications. La recherche française a attaqué les problématiques liées à l'utilisation de ce format avec des techniques très variées. Elle a ainsi fait des progrès importants en langages de programmation grâce à la définition de systèmes polymorphes pour le traitement de données en format XML ou en analyse statique des transformations de documents en format XML, notamment grâce à l'utilisation de solveurs pour des logiques modales.

Une autre avancée marquante concerne un problème classique en théorie des langages formels : décider si le langage des mots acceptés par un automate peut aussi être exprimé par une formule logique. On sait par exemple que la logique monadique du second ordre a le même pouvoir expressif que les automates finis. Une avancée marquante vient d'être obtenue : la décidabilité de l'appartenance d'un langage aux classes BΣ2 et Σ3. La résolution de ce problème ouvert depuis quarante ans vient renouveler le sujet de manière profonde grâce à une innovation conceptuelle importante.

Enfin, la dernière avancée majeure retenue ici concerne la théorie homotopique des types. La théorie des types intuitionniste est une formalisation de la logique intuitionniste développée par Martin-Löf dans les années 70 qui se caractérise par la présence de types paramétrés. Un des défis majeurs a été la compréhension du statut de l'égalité. Une nouvelle approche vient de changer notre perception de cette problématique. Voevodsky a réalisé que l'algèbre homotopique fournissait des modèles très riches de la théorie des types, où, intuitivement, l'égalité devient une déformation (une homotopie) permettant de transformer un objet en un autre, généralisant considérablement les idées antérieures. Cela a amené Voevodsky à ajouter un axiome à la théorie des types : l'axiome d'univalence exprime une forme de complétude du type identité vis-à-vis de ces déformations. Il a ainsi établi un pont très surprenant entre logique d'une part et topologie algébrique d'autre part, riche de promesses tant pour la logique et l'informatique que pour les mathématiques. Cette théorie a déjà une influence certaine sur le développement des assistants de preuves comme Coq.

B. Nouvelles directions

Plusieurs développements récents traduisent un basculement vers de nouveaux points de vue ou paradigmes. Ainsi, en vérification, les spécifications et les techniques d'analyse ne sont plus seulement qualitatives mais également quantitatives : il ne suffit plus seulement de savoir si un système peut atteindre un état interdit, mais avec quelle probabilité cela peut avoir lieu, ou dans quel contexte (bande passante allouée, contrainte d'énergie, etc.), ou encore d'étudier la robustesse des propriétés de systèmes soumis à des perturbations. Dans une autre direction, des liens remarquables ont été établis entre la théorie des jeux et les techniques de vérification ou de contrôle permettant ainsi de modéliser et de synthétiser des protocoles mettant en jeux de multiples agents. L'interaction d'un système avec un ou plusieurs acteurs de l'environnement est alors vue comme un jeu à plusieurs joueurs, et les spécifications comme des objectifs de gain.

Dans le domaine de la sécurité, la communauté est passée de l'analyse de propriétés de sécurité classiques (authentification, confidentialité), basées sur de l'accessibilité, à des propriétés ayant trait à la vie privée (secret du vote, anonymat, non traçabilité, etc.). Un pont important pour les applications a également été établi vers les modèles plus fins de sécurité utilisés en cryptographie.

Enfin, dans le domaine des bases de données, les points de vue ont fortement évolué, en phase avec le développement de nouveaux formats dont la structuration relationnelle est faible (NoSQL) et l'explosion des bases de données massives, hétérogènes, incomplètes, incertaines, et dynamiques. Ainsi, des logiques et automates ont été développés pour capturer ces évolutions. Les nouvelles problématiques posées par l'interrogation efficace de ces bases de données et l'évolution de leurs formats sont nombreuses.

C. Outils développés en France et impact sociétal

La recherche française se distingue ici par le développement de nombreux prototypes, aboutissant pour certains à des outils à fort impact. En sécurité, différents prototypes d'analyse automatique de protocoles ont vu le jour, et trois des quatre principaux outils ont été mis au point en France (ProVerif, APTE, Akiss). En vérification et en analyse statique, une plate-forme a récemment vu le jour (Cosyverif), visant à proposer un format unique de manipulation de systèmes. L'outil d'analyse statique de code Astrée est par ailleurs maintenant commercialisé et régulièrement utilisé par l'industrie.

Enfin, après plus de 20 ans de développement, l'outil de preuve formelle Coq (Calculus of Constructions) a atteint la pleine reconnaissance en recevant en 2014 le prix ACM Software System Award, le plaçant ainsi au même niveau que des standard tels que TeX, TCP/IP, WWW, Apache, Java, Unix et Postscript. Les systèmes de vérification de preuves formelles sont apparus à la fin des années 1960. En plus de la vérification, ils aident l'utilisateur à construire interactivement des preuves à l'aide de stratégies. Ainsi, l'assistant de preuves Coq est de plus en plus utilisé pour prouver d'importants résultats mathématiques, comme le théorème fondamental de l'algèbre dans la bibliothèque CoRN (Constructive Coq Repository at Nijmegen), le théorème des quatre couleurs, la classification des groupes finis (théorème de Feit-Thompson). Mais Coq est aussi un outil pour formaliser et vérifier d'autres systèmes, par exemple un compilateur pour le langage C, une version légère du langage de programmation Java, ou encore un micro noyau de système d'exploitation. Ces derniers travaux sont particulièrement importants pour les applications industrielles dans des domaines critiques, tels que l'avionique, la monétique et le nucléaire.