Soutenance de thèse de Mathieu Sassolas

Bonjour,

j'ai le plaisir de vous inviter à la soutenance de ma thèse intitulée

Méthodes qualitatives et quantitatives
pour la détection d'information cachée

ainsi qu'au pot qui suivra.

La soutenance aura lieu le lundi 28 novembre 2011 à 10h à Jussieu en
salle 25-26/105.

========================================================================
Résumé
========================================================================

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 ».

========================================================================
Abstract
========================================================================

Information systems have become ubiquitous and are used to handle each
day more and more data. This data is increasingly confidential: it may
be strategic military or financial information, or private information.
Any leakage of this data can be harmful in many different ways, such
that human casualties, money loss, privacy breaching or identity theft.

The use of formal methods and especially formal verification of such
systems has become necessary to ensure both the safety of the behavior
of the system and the security of the information it handles. These
techniques are applied on models of the system where some parameters –
especially quantitative parameters – may have been abstracted. These
omitted parameters have sometimes been used in order to breach the
security of supposedly secure systems. Nowadays, models tend to include
more of this information, which is often relative to the (continuous)
elapsing of time or to the probability distributions that rule the
system's behavior.

Models also include the architecture of the systems as several
processes, who may have different, or even contradictory, goals: one may
want to keep a secret while the other tries to discover it. When the
behavior of all processes is partially or completely unknown, formal
methods have to consider all possible cases, which is in general
impossible (if there exist an infinite number of choice) or intractable
(if there exist too many possibilities to consider them all).

The contributions of this thesis are threefold. First, we study the
problem of synthesis of a communication channel inside a system given as
a transducer. Even though the model of transducers is syntactically
limiting, we show that this synthesis problem is undecidable in general.
However, when the system is functional, meaning that its behavior from
an external point of view is always the same, the problem becomes decidable.

We then generalize the concept of opacity to probabilistic systems, by
giving measures separated in two groups. When the system is opaque, we
evaluate the robustness of this opacity with respect to the bias induced
by the probability distributions in the system. When the system is not
opaque, we evaluate the size of the security hole opened by this
non-opacity.

Finally, we study the model of Interrupt Timed Automata (ITA) where
information about time elapsing is organized along levels, which
therefore resemble accreditation levels. We study properties of
regularity and closure of the time languages accepted by these automata
and give some model-checking algorithms for fragments of timed temporal
logics. These results allow to verify formulas such as "the system is
(in state) ready before 7 time units have elapsed since the beginning of
the system's execution".

========================================================================
Composition du jury
========================================================================

Catuscia PALAMIDESSI, INRIA et École polytechnique; rapporteur.
Jean-François RASKIN, Université Libre de Bruxelles; rapporteur.
Philippe DARONDEAU, IRISA/INRIA Rennes; examinateur.
Serge HADDAD, École normale supérieure de Cachan; examinateur.
Fabrice KORDON, Université Pierre et Marie Curie; examinateur.
Béatrice BÉRARD, Université Pierre et Marie Curie; directrice de thèse.

Cordialement,
--
Mathieu Sassolas