Karthik Bhargavan : prouver la sûreté des applications web
Date:
Mis à jour le 26/03/2020
Prévenir plutôt que guérir : cet adage médical s’applique aussi à l’informatique. Le jeune chercheur de l’équipe Moscova, Karthik Bhargavan, vient de recevoir une bourse ERC pour poursuivre ses travaux visant à assurer la sûreté de services tels que la gestion de données personnelles et sensibles. Des recherches à la fois théoriques et très appliquées, au sein du laboratoire commun entre Inria et Microsoft Research. Rencontre avec le chercheur.
C’est avec des carrés, des ronds et des flèches que Karthik Bhargavan explique les travaux qu’il va mener grâce à la bourse européenne ERC d’1,5 million d’euros sur cinq ans qu’il vient de recevoir. Son domaine : la sécurité informatique. « Nous échangeons de nombreuses informations en ligne, il faut être sûr qu’elles ne soient pas volées ou modifiées », explique le chercheur indien de 34 ans. « C’est particulièrement vrai pour certains sujets sensibles comme les données bancaires ou médicales. »
Prenons le cas du dossier médical numérique, en cours d’élaboration en France, et qui existe déjà aux États-Unis. Les données de chaque patient sont cryptées et stockées dans un serveur sécurisé, et certaines personnes (le patient, le médecin, l’hôpital…) ont le droit de lire ou d’ajouter des données. Mais les cibles potentielles des attaques sont nombreuses : le navigateur web, le protocole de cryptographie, la gestion des clés de chiffrement, la programmation des pages web (programme javascript)… Comment prouver que l’ensemble du système est vraiment sûr ? Comment être certain qu’un pirate ne cassera pas les protections ? C’est le but du projet CRYSP développé par Karthik Bhargavan et qui a séduit l’ERC. « Plutôt que d’arrêter les attaques, mieux vaut les prévenir. Je propose de construire la première application web, dont la sécurité sera mathématiquement prouvée. L’ensemble du système devra être totalement sécurisé. »
Construire la première application web, dont la sécurité sera mathématiquement prouvée.
Pour prouver mathématiquement qu’un programme informatique est sûr, il faut d’abord le "traduire" en un modèle plus facile à analyser. Puis ce modèle est ausculté par un outil d’analyse de programme, qui prend en compte les exigences de sécurité choisies par les chercheurs. Cet outil peut donner trois types de réponses : « oui, la sûreté de ce logiciel est prouvée », « non, des attaques ont réussi », et enfin « nous ne savons pas si ce logiciel est sûr ». Cette dernière réponse est malheureusement la plus fréquente. Le but des recherches de Karthik Bhargavan est justement de la rendre moins fréquente et de parvenir plus souvent à la réponse affirmative.
Karthik Bhargavan va recruter deux chercheurs postdoctoraux, quatre doctorants et sept stagiaires en master au cours des cinq prochaines années pour réaliser son projet. Ce chercheur au parcours international (des études à New Delhi en Inde, un doctorat à Philadelphie aux États-Unis, et sept ans de recherche sur la sécurité du Web chez Microsoft Research à Cambridge en Grande-Bretagne) ne se fait pas de souci sur le recrutement : « j’apprécie beaucoup de travailler avec des étudiants français, à qui je donne des cours à l’École polytechnique », souligne-t-il. « La qualité des étudiants est une des raisons pour lesquelles j’ai choisi la France. Et puis je compte attirer des étudiants des États-Unis, de Grande-Bretagne et d’Inde, où j’ai gardé beaucoup de contacts ».
Il a également choisi la France et Inria pour cette alliance inédite de compétences en ingénierie et en mathématiques, due notamment à la collaboration étroite entre chercheurs d'Inria et de Microsoft Research au sein du laboratoire commun de Saclay. « Cette association de recherches très appliquées et fondamentales menées chez Inria est très intéressante, souligne-t-il. Je travaille à la fois sur les programmes et sur les preuves mathématiques. Et j’ai la satisfaction de m’intéresser à des problèmes réels. »