Titre de la thèse : Algorithmique pour les propriétés de sécurité des systèmes répartis
Directeur : Pascal Berthomé
Co – encadrant : Jérémy Briffaut
Contexte :
La thèse s’insère dans l’approche développée dans le cadre du projet SDS pour garantir des propriétés de sécurité système ou en détecter les violations. Un langage a été défini permettant d’exprimer les propriétés de sécurité requises pour un système au moyen de la notion de séquence d’appels système et d’opérateurs entre séquences. Ces propriétés peuvent être garanties en calculant des chemins dans des graphes d’interactions. Le système PIGA met en œuvre cette approche de manière concrète sur des systèmes réels. Ce travail a donné lieu à deux thèses soutenues dont une co-financée par le CEA. De plus, une thèse en cours est financée par la région Centre et une autre est financée par le CEA DAM. Enfin, cette thèse s’insère dans l’accord cadre passé entre le CEA et le projet SDS sur le thème de la sécurité système et de leurs application aux architectures réparties à large échelle telle que les clusters ou les grilles de calcul.
Objectifs :
Il s’agit de compléter les travaux menés et en cours, en les élargissant aux systèmes répartis. En effet, actuellement nous savons exprimer des propriétés pour un système mais pas à l’échelle d’un système réparti. L’idée est d’offrir un langage adapté à un système réparti afin d’exprimer des propriétés de sécurité complexes prenant en compte des séquences d’opérations qui sont réparties sur plusieurs machines. Par exemple, il est possible d’envisager une propriété de confidentialité qui garantit l’absence de flot d’information entre deux processus présents sur deux machines différentes. Différentes applications sont possibles pour d’une part garantir ces propriétés, d’autre part en détecter les violations et enfin offrir un moyen de reconnaître et reconstruire des attaques réparties. Des coopérations existent déjà dans le projet SDS notamment avec le CEA qui offriront un cadre d’applications possibles. Ces techniques pourront être utilisées aussi bien par le CEA et les projets de grilles de calcul Européennes, mais bien sûr aussi plus largement pour tous les systèmes répartis à large échelle.
Plan de travail :
Dans un premier temps un état de l’art sera mené sur les propriétés réparties de sécurité et sur les moyens d’exprimer ces propriétés. Cet état de l’art fournira les bases pour étendre le langage existant avec des opérateurs manipulant des caractéristiques de répartition. Ensuite, ces opérateurs seront utilisés définir le graphe d’interactions dans le cas des systèmes distribués, comme composition particulière des graphes d’interaction des différentes machines composant le système. Si les graphes d’interaction sont de faible taille à l’échelle d’une seule machine, la composition aura sans doute plusieurs conséquences directes. La première sera que la taille du graphe d’interaction global sera importante, voire impossible à stocker dans les systèmes actuels. Par ailleurs, les propriétés que l’on cherche à mettre en évidence sur ces structures auront sans doute des contraintes fortes n’autorisant pas un calcul par un simple parcours, comme dans le cas d’une seule machine. Une étude algorithmique théorique devra être menée pour mettre en évidence les implications de l’ajout de nouvelles machines à un système, éventuellement en proposant des alternatives « utilisables dans un système réel ». Enfin, les propriétés ainsi exprimées pourront être comparées aux attaques d’un système pour reconnaître les attaques ou vérifier l’intérêt pratique d’une propriété. A nouveau, des problèmes difficiles de comparaisons (du type recherche de sous-graphes isomorphes) de graphes apparaissent.