Deux ans après l'inauguration du laboratoire commun entre l'Inria et Microsoft, c'est un Bernard Ourghanlian (directeur technique et sécurité de Microsoft France) « content, et même plutôt impressionné » par les résultats obtenus, qui présente les projets menés conjointement par les chercheurs des deux entités. Toute une journée a été consacrée à l'événement hier, 28 janvier, à l'Ecole polytechnique. Dans la salle, « 200 personnes, essentiellement des chercheurs, venus du monde entier », précise Bernard Ourghanlian. Un rapport scientifique décrivant l'activité du centre de recherches commun sera présenté courant février. En attendant, cette journée a été l'occasion d'aborder les 7 projets sur lesquels travaillent les chercheurs depuis janvier 2007 (et parfois avant, certains liens ayant été établis longtemps auparavant). Les travaux sont répartis en deux thèmes: « la sécurité et la fiabilité du logiciel d'une part, les interactions entre l'informatique et les autres sciences d'autre part ». Dans tous les cas, précise Bernard Ourghanlian, « ce sont les ingénieurs de recherche qui choisissent les sujets sur lesquels ils vont travailler ». Dans le premier thème, il s'agit d'appliquer les mathématiques pour améliorer la sécurité et la fiabilité des logiciels. Trois projets sont regroupés sous cette ombrelle. Parmi eux, le recours à des programmes informatiques pour prouver des théorèmes mathématiques. La démonstration du théorème sur lequel travaille l'équipe d'une dizaine de chercheurs « tient sur 400 articles et 10 000 pages », explique Bernard Ourghanlian. Et encore, dit-il, « il n'est prouvé que parce qu'il a été lu par des pairs mathématiciens, qui l'ont déclaré correct avec une certitude de 99% ». Le projet vise à créer une bibliothèque de preuves élémentaires qu'un logiciel pourra utiliser pour obtenir une preuve parfaite. « Et inversement, on pourra utiliser les mathématiques pour prouver qu'un logiciel est correct. » A l'heure actuelle, seuls les projets informatiques où la sécurité des personnes est en jeu (gestion du trafic du métro, informatique embarquée dans les avions ou les voitures, gestion opérationnelle des centrales nucléaires, etc.) se permettent de prendre le temps de recourir à des méthodes formelles pour s'assurer de la fiabilité des logiciels. Apporter des preuves formelles de sécurité dans un environnement distribué Toujours dans le thème de « l'informatique de confiance » cher à Microsoft (qui s'échine ainsi à faire oublier ses failles de sécurité et autres bugs à répétition), le deuxième projet a pour but, dans une architecture distribuée, d'apporter des preuves formelles de sécurité. Qui permettront par exemple de prouver qu'une machine n'est pas sûre, ou au contraire qu'un protocole de sécurité est bien respecté. « Quand je suis connecté au site de ma banque, prend comme exemple Bernard Ourghanlian, je veux être certain que c'est bien le site de ma banque. Et réciproquement, ma banque veut être sûr que c'est bien moi. Ce n'est pas toujours simple. » Dans le troisième projet tombant dans cette catégorie, il s'agit de recourir à une méthode (TLA, Temporal logic of actions) et à un langage (TLA+) pour s'assurer que ce qui est obtenu à partir d'un modèle est bien ce qui était voulu au départ. L'idée, expliquent les auteurs du projet, est de pouvoir « attraper les bugs dans un algorithme ou la modélisation d'un système avant même qu'il ne soit implémenté ». Un dictionnaire mathématique en ligne et des interfaces homme/machine pour les scientifiques