En 2007, Microsoft et l'Inria créent un laboratoire commun. Les deux acteurs présentent aujourd'hui les premiers résultats dans deux domaines distincts : la sécurité et les outils informatiques destinés aux scientifiques.

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


Le deuxième thème de recherches, dont l'ambition est de mettre l'informatique au service des scientifiques, comporte quatre projets. Le premier vise à créer une sorte de dictionnaire dynamique de fonctions mathématiques, « de façon, explique Bernard Ourghanlian, à ce que les physiciens disposent d'une fonction de génération automatique de fonctions mathématiques, au travers d'une interface Web, avec la possibilité de modifier les paramètres et les variables d'une manière graphique ».

Un premier prototype est d'ailleurs opérationnel.

. Web-profils.com, la place de marché du conseil et de l'ingénierie