SASSOLAS Mathieu

doctorant à Sorbonne Université
Équipe : MoVe
https://www.lacl.fr/~msassolas/
https://www.lacl.fr/~msassolas/

Direction de recherche : Béatrice BÉRARD

Noninterférence et canaux cachés dans les systèmes temporisés

Les systèmes informatiques sont devenus omniprésents et sont utilisés au quotidien pour gérer toujours plus d'information. Ces informations sont de plus en plus souvent confidentielles : il peut s'agir d'informations stratégiques militaires ou financières, ou bien d'informations personnelles. La fuite de ces informations peut ainsi avoir des conséquences graves telles que des pertes humaines, financières, des violations de la vie privée ou de l'usurpation d'identité. Les méthodes formelles de vérification sont nécessaires pour garantir la sûreté et la sécurité du système. Ces techniques s'appliquent sur des modèles du système où certains paramètres ? en particulier des paramètres quantitatifs ? peuvent avoir été abstraits. Ces paramètres ont pu être utilisés dans des attaques de systèmes réputés sûrs. Les modèles actuels intègrent donc ces informations, qui se rapportent le plus souvent à l'écoulement (continu) du temps ou aux lois de probabilités qui régissent le fonctionnement du système. Les modèles intègrent d'autre part le découpage de l'application en divers processus, mûs par des buts différents, voire contraires : l'un peut chercher à dissimuler de l'information tandis que l'autre cherche à la découvrir. Lorsque le fonctionnement de tous les processus est partiellement ou totalement inconnu, les méthodes formelles doivent considérer tous les cas possibles, ce qui est en général impossible en théorie ? s'il existe un nombre infini de possibilités ? ou en pratique ? s'il existe trop de possibilités pour que l'on puisse les envisager exhaustivement. Les contributions de cette thèse se découpent en trois parties. Tout d'abord, nous étudions le problème de synthèse d'un canal de communication dans un système décrit par un transducteur. Malgré les limites imposées par ce modèle, nous montrons que le problème de synthèse est indécidable en général. Cependant, lorsque le système est fonctionnel, c'est-à-dire que son fonctionnement externe est toujours le même, le problème devient décidable. Nous généralisons ensuite le concept d'opacité aux systèmes probabilistes, en donnant des mesures groupées en deux familles. Lorsque le système est opaque, nous évaluons la robustesse de cette opacité vis-à-vis des informations données par les lois de probabilités du système. Lorsque le système n'est pas opaque, nous évaluons la taille de la faille de sécurité induite par cette non opacité. Enfin, nous étudions le modèle des automates temporisés à interruptions (ITA) où les informations sur l'écoulement du temps sont organisées en niveaux comparables à des niveaux d'accréditation. Nous étudions les propriétés de régularité et de clôture des langages temporisés générés par ces automates et proposons des algorithmes de model-checking pour des fragments de logiques temporelles temporisées. Ces résultats permettent la vérification de propriétés telles que « le système est (dans un état) prêt avant les 7 premières unités de temps de fonctionnement du système ».

Soutenance : 28/11/2011

Membres du jury :

PALAMIDESSI Catuscia (LIX, INRIA et École Polytechnique) [Rapporteur]
RASKIN Jean-François (Université Libre de Bruxelles) [Rapporteur]
DARONDEAU Philippe (INRIA/IRISA)
HADDAD Serge (LSV, ENS Cachan)
KORDON Fabrice (LIP6, Université Pierre et Marie Curie)
BÉRARD Béatrice (LIP6, Université Pierre et Marie Curie)

Date de départ : 31/12/2011

Publications 2009-2021