Hubert Comon : « Définir un attaquant universel pour les preuves de sécurité »
Depuis octobre 2016, Hubert Comon est membre senior de l’Institut Universitaire de France. Ce spécialiste des méthodes formelles appliquées à la sécurité informatique propose un nouveau paradigme dans son projet ComSeFor (Computer Security and Formal methods) pour réaliser des preuves de sécurité quel que soit le modèle d’attaquant.
L’attaquant est déjà largement pris en compte dans les preuves de sécurité. Qu’y a-t-il de nouveau dans votre approche ?
Hubert Comon : Beaucoup de personnes dans le monde travaillent sur les problèmes de sécurité et sont toutes confrontées au même problème : comment définir l’attaquant ? En effet, pour savoir comment définir la sécurité, il est nécessaire de définir ce qu’est un attaquant. Sur ce point, il y a des consensus sur ce qu’est un adversaire, mais aussi des divergences de points de vue entre les mondes de la vérification et de la cryptographie par exemple. Cependant, dans tous les cas, on attribue des capacités à l’attaquant. Les cryptographes utilisent par exemple un modèle calculatoire de l’attaquant auquel on affecte une certaine ressource. Les preuves de sécurité qui sont faites sont liées à cette définition de l’attaquant, à ce modèle. Mais une preuve de sécurité n’exclut pas l’existence d’attaques qui ne sont pas prévues dans le modèle. Les attaques peuvent exploiter en effet des ressources que l’on n’imagine pas forcément au premier abord, comme le fait de mesurer l’énergie consommée par une machine pour en récupérer des informations.
Mon projet vise à contourner le problème, en spécifiant ce qu’un attaquant ne peut pas faire, au lieu de préciser ce qu’il peut faire. Il n’est pas possible d’utiliser une définition d’attaquant qui puisse absolument tout faire, car dans ce cas il n’y aurait aucune parade contre les attaques. Un petit nombre de restrictions raisonnables est donc nécessaire, comme « un attaquant ne peut pas deviner un nombre aléatoire que j’engendre s’il est suffisamment long », pour permettre une preuve. Cet attaquant qui peut tout faire, sauf ce qui a été explicitement exclu, cet attaquant « dans le pire des cas » est donc quelque part un attaquant universel, qui, si on apporte la preuve de la sécurité d’un système contre lui, assure que cette preuve est valide face à tout autre attaquant plus faible.
Nous espérons ainsi réunir les points de vue de la vérification et de la cryptographie sur le sujet. Notre but est également de réaliser des preuves de sécurité dans des cadres où il n’y avait pas de solution jusque-là.
Comment pensez-vous procéder pour mettre en œuvre ce projet ?
H. C. : Les preuves d’indistinguabilité sont un bon cas d’étude. Dans les modèles classiques d’attaquant, ces preuves sont difficiles à mettre au point. Pour expliquer ce qu’est l’indistinguabilité, nous allons prendre l’exemple d’un vote. Ce n’est pas la confidentialité qui est importante : les bulletins de vote sont connus de tous. Ce qui est important c’est que le lien entre un votant et son bulletin reste secret : c’est l’anonymat. Pour exprimer l’anonymat, on utilise une propriété d’indistinguabilité : on ne doit pas pouvoir distinguer un scénario dans lequel Alice a voté A et Bob B d’un scénario dans lequel Alice a voté B et Bob A. Nous souhaitons revisiter les preuves d’indistinguabilité avec notre nouvelle approche, pour permettre de formaliser et d’automatiser les preuves, pour des familles d’attaquants générales. Nous espérons mettre au point un logiciel pour réaliser automatiquement de telles preuves d’indistinguabilité.
D’autre part, les programmes auxquels nous sommes confrontés sont de plus en plus complexes, résultats d’échanges avec d’autres programmes et d’empilements de différents bouts de logiciels. Pour réaliser une preuve de sécurité, nous nous concentrons généralement sur une seule partie du programme, mais sans pouvoir prendre en compte les interactions avec d’autres logiciels qui pourraient ouvrir de nouvelles failles de sécurité. Avec notre nouvelle approche, nous souhaitons trouver un moyen conceptuel de simplifier ce problème. En tirant parti de cet attaquant arbitraire, on pourrait décomposer les problèmes de sécurité en des problèmes plus atomiques afin de pouvoir les résoudre.
Le modèle de l’attaquant dans le pire des cas permet aussi de conduire des preuves de sécurité dans des situations où il n’est pas possible d’établir une correspondance entre modèles calculatoires de la cryptographie et modèles symboliques de la vérification.