Monitoring and Supervisory Control for Opacity

-

Documents
161 pages
Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus

Description

Niveau: Supérieur, Doctorat, Bac+8
No d'ordre : 3966 ANNÉE 2009 THÈSE / UNIVERSITÉ DE RENNES 1 sous le sceau de l'Université Européenne de Bretagne pour le grade de DOCTEUR DE L'UNIVERSITÉ DE RENNES 1 Mention : Informatique Ecole doctorale Matisse présentée par Jérémy Dubreil préparée à l'unité de recherche IRISA (UMR 6074) Institut de Recherche en Informatique et Systèmes Aléatoires Composante universitaire : IFSIC Monitoring and Supervisory Control for Opacity Properties Thèse soutenue à Rennes le 25 novembre 2009 devant le jury composé de : Roland Groz Professeur à l'institut polytechnique de Grenoble / pré- sident du jury Jean François Raskin Professeur à l'Université Libre de Bruxelles / rapporteur Yassine Lakhnech Professeur à l'Université Joseph Fourier / rapporteur Philippe Darondeau Directeur de recherche à l'INRIA/ examinateur Olivier H. Roux Maître de conférences à l'IUT de Nantes / examinateur Thierry Jéron Directeur de recherche à l'INRIA/directeur de thèse Hervé Marchand Chargé de recherche à l'INRIA/ co-directeur de thèse

  • abstract interpretation

  • pré- sident du jury

  • roux maître de conférences

  • opacity

  • based observation

  • thèse soutenue

  • language based

  • informatique ecole doctorale

  • directeur de la recherche


Sujets

Informations

Publié par
Nombre de visites sur la page 80
Langue Français
Signaler un problème

oN d’ordre:3966 ANNÉE2009
THÈSE / UNIVERSITÉ DE RENNES 1
sous le sceau de l’Université Européenne de Bretagne
pour le grade de
DOCTEUR DE L’UNIVERSITÉ DE RENNES 1
Mention : Informatique
Ecole doctorale Matisse
présentée par
Jérémy Dubreil
préparée à l’unité de recherche IRISA (UMR 6074)
Institut de Recherche en Informatique et Systèmes Aléatoires
Composante universitaire : IFSIC
Thèse soutenue à Rennes
le 25 novembre 2009
devant le jury composé de :
Monitoring and Roland Groz
Professeur à l’institut polytechnique de Grenoble / pré-
sident du jurySupervisory Control
Jean François Raskin
Professeur à l’Université Libre de Bruxelles/rapporteurfor Opacity Properties
Yassine Lakhnech
Professeur à l’Université Joseph Fourier/rapporteur
Philippe Darondeau
Directeur de recherche à l’INRIA/examinateur
Olivier H. Roux
Maître de conférences à l’IUT de Nantes/examinateur
Thierry Jéron
Directeur de recherche à l’INRIA/directeur de thèse
Hervé Marchand
Chargé de recherche à l’INRIA/co-directeur de thèse2Remerciements
Je tiens à remercier Yassine Lakhnech et Jean-François Raskin pour avoir rapporté mon
travail de thèse. Je remercie également Roland Groz pour avoir présidé ma soutenance de
thèse ainsi que Philippe Darondeau et Olivier H. Roux pour avoir examiné pour travail.
Je remercie aussi chaleureusement mes encadrants de thèse, Thierry Jéron et Hervé
Marchand pour leur disponibilité et leurs précieux conseils, distillées avec gentillesse et
bonne humeur au court de mon doctorat. Grand merci de nouveau à Philippe Daron-
deau qui, au fil de nos collaborations, a beaucoup influencé mon travail de thèse et plus
généralement ma vision du métier de chercheur.
Je voudrai remercier également l’ensemble de l’équipe VerTeCs. Il s’agit en effet d’une
équipeoùl’ambianceestparticulièrementbonneetauseindelaquellej’aiappréciétravailler
pendant ces années de thèse.
34Contents
1 Introduction 23
1.1 Summary of the Thesis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
1.2 Related Works . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
1.3 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
2 Basic Notions 39
2.1 Sets and Relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
2.1.1 Posets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
2.1.2 Lattices . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
2.2 Labeled Transition Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
3 Information Flow and Opacity 51
3.1 Confidential Information and Notion of Attackers . . . . . . . . . . . . . . . 51
3.2 Definition of Opacity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
3.3 Properties of Opacity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
3.3.1 Some General Properties of Opacity . . . . . . . . . . . . . . . . . . 57
3.3.2 Trace-based Observation Maps . . . . . . . . . . . . . . . . . . . . . 57
3.4 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60
4 Verifying and Monitoring Opacity 63
4.1 Determinization Based Procedure to Construct Sound Monitors . . . . . . . 63
4.2 Complexity of Verifying Opacity on Finite Models . . . . . . . . . . . . . . 66
4.3 Monitoring Opacity Using Abstract Interpretation . . . . . . . . . . . . . . 68
4.3.1 Basics of Abstract Interpretation . . . . . . . . . . . . . . . . . . . . 69
4.3.2 Construction of Monitors for Opacity . . . . . . . . . . . . . . . . . . 73
4.3.3 Static Computation of Vulnerabilities Combining Under and Over
Approximations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77
4.4 Language Based Approach and Regular Abstractions . . . . . . . . . . . . . 78
4.4.1 Monitor for the Attackers . . . . . . . . . . . . . . . . . . . . . . . . 80
4.4.2 Diagnosing Information Flow . . . . . . . . . . . . . . . . . . . . . . 81
4.5 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87
5Contents
5 Supervisory Control to Enforce Opacity 89
5.1 The Supervisory Control Problem . . . . . . . . . . . . . . . . . . . . . . . . 90
5.1.1 Language Based Approach for the Supervisory Control Problem . . . 91
5.1.2 The Fixpoint Iteration Techniques . . . . . . . . . . . . . . . . . . . 93
5.1.3 The Safety Control Problem . . . . . . . . . . . . . . . . . . . . . . . 96
5.2 The Opacity Control Problem . . . . . . . . . . . . . . . . . . . . . . . . . . 97
5.2.1 Characterization of the Solution . . . . . . . . . . . . . . . . . . . . 98
5.2.2 An Operator for the Supremal Opaque Sublanguage . . . . . . . . . 99
5.3 Computation of the Supremal Controller when and are Comparable . 101a o
5.3.1 The Case . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101o a
5.3.2 The Case . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102a o
5.4 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 124
6 Dynamic Projections to Enforce Opacity 125
6.1 Maximum Cardinality Set for Static Projections . . . . . . . . . . . . . . . . 126
6.2 Opacity with Dynamic Projection . . . . . . . . . . . . . . . . . . . . . . . . 127
6.3 Enforcing Opacity with Dynamic Projections . . . . . . . . . . . . . . . . . 134
6.3.1 Reduction to a 2-player Safety Game . . . . . . . . . . . . . . . . . . 136
6.3.2 The Set of Valid Dynamic Projections . . . . . . . . . . . . . . . . . 143
6.4 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 146
7 Conclusion 149
6Résumé des Travaux de Thèse
Nota bene: This an extended summary of the thesis. This part in french is mandatory
because the rest of the thesis is written in English.
Le développement des réseaux ouverts tels qu’Internet ou les réseaux mobiles a induit l’ex-
plosion du nombre de service proposés sur ces réseaux. Certain de ces services manipulent
desinformationscritiquesquidoiventpasêtrecorrompuesdefaçonintentionnelleouarriver
en possession d’entités malveillantes. Citons pour exemple les systèmes d’administration
électroniques, les systèmes de vote ou les bases de données d’information médicales. Dans
ce contexte, le développement de techniques fiables et efficaces pour certifier la sécurité
d’un système est essentiel. Afin d’étudier de tels algorithmes de certification, les propriétés
de sécurité sont généralement classifiées en trois catégories :
– l’intégrité;
– la disponibilité;
– la confidentialité.
Une politique de sécurité consiste en un ensemble de propriétés de sécurité, de différentes
catégories,quidoiventêtreconjointementsatisfaitessurlesystème.Nousdonnonsquelques
explicationssurchacunedecescatégoriesafindesituerdansquelcadreseplacenostravaux
de thèse.
Les propriétés d’intégrité expriment l’idée qu’un attaquant ne peut exercer d’actions non
autorisées ou forcer le système à atteindre une configuration critique. Si l’on choisit comme
exemple un système de vote, le fait que personne ne puisse modifier le vote d’un autre
électeur est une propriété d’intégrité. Les contraintes d’intégrité sont donc généralement
exprimées par des propriétés de sûreté. Il existe néanmoins des propriétés d’intégrité qui ne
s’expriment pas par des propriétés de sûreté, notamment lorsqu’il est question d’intégrité
de l’information (voir [GMP92] pour plus de détails). Nous montrons dans cette thèse
comment vérifier qu’une propriété de sûreté est satisfaite et comment assurer une telle
propriétésurunsystèmedonné.Cesrésultatss’appliquerontdoncauxpropriétésd’intégrité
qui peuvent être exprimées par des propriétés de sûreté.
Les propriétés de disponibilité expriment l’idée qu’un attaquant ne peut entraver le bon
comportement d’un système. En prenant de nouveau l’exemple d’un système de vote, un
7Contents
attaquant ne peut empêcher un électeur de voter. Typiquement, les attaques de type déni
de service sont des violations de propriétés de disponibilité. Nous n’aborderons pas ici ce
type de propriétés.
Les propriétés de confidentialité sont celles qui nous intéressent plus particulièrement
dans cette thèse. Elles expriment l’idée qu’un attaquant ne peut acquérir d’information
secrète. Par exemple, un attaquant ne peut inférer le vote d’un autre électeur. Dans ce
document, nous allons considérer ces aspects de confidentialité avec la notion d’opacité.
Cette notion a été introduite dans [Maz04] et ensuite généralisée au cas des systèmes de
transitions dans [BKMR08].
La particularité des propriétés de confidentialité est qu’elles doivent être définies relati-
vement à la connaissance des attaquants potentiels. Nous expliquons maintenant cet aspect
avec un bref historique sur ce type de propriétés. Dans [BL73], les auteurs proposent une
formalisation des systèmes alors en place dans le secteur militaire afin de préserver la confi-
dentialité des informations. Ce modèle, connu sous les initiales BLP pour Bell et LaPadula,
repose sur la notion d’objet (des documents par exemple) et de sujet (personnes ou pro-
grammes). Les sujets exercent des actions de type lecture, écriture, création, destruction,
etc, sur ces objets. À chaque objet et chaque sujet est assigné un niveau de confidentialité,
par exemple confidentiel, publique, etc. La confidentialité de l’ensemble est alors assuré par
un contrôle d’accès qui interdit certain types d’opération. Par exemple, il est impossible
pour un sujet de niveau publique de lire un objet situé au niveau confidentiel, ou encore, il
est impossible pour un sujet de niveau confidentiel d’écrire dans un objet situé au niveau
publique. Cet ensemble de règles a pour but d’empêcher le flot d’information du niveau
confidentiel vers le niveau publique. Mais cette formalisation est limitée dans le sens où elle
ne permet pas de réellement prouver l’absence de flot d’information. En effet, si un sujet
A de niveau publique essaye d’écrire dans un fichier F au niveau confidentiel lorsque ce
fichier est inexistant, alors A observe un message d’erreur. Si ce fichier F existe, l’écriture
étant autorisé dans ce sens, A n’observe aucun message d’erreur. Ainsi, en collaboration
avec un sujet B situé au niveau confidentiel, pour qui la création et la destruction d’objet
est possible, le sujetB peut créer un canal de communication allant du niveau confidentiel
au niveau publique, contournant ainsi les mesures de protection.
Le modèle BLP se révèle donc insuffisant pour interdire certains flots d’information car il
ne permet pas de prendre en compte la capacité des sujets, potentiellement des attaquants,
à inférer de l’information en fonction de ce qu’ils observent et de ce qu’ils connaissent du
système. Pour palier à ce manque, Goguen et Meseguer proposent dans [GM82] une notion
plus précise, appelé non-interférence, exprimant l’absence de flot d’informations confiden-
tielles. Reprenant les dénominations utilisées plus haut, la propriété de non-interférence
est vérifiée si ce que font les sujets de niveau confidentiel n’a pas d’influence sur ce que
8Contents
les sujets de niveau publique peuvent observer. On voit bien qu’avec une telle définition,
le cas de flot d’information exprimé plus haut disparaît. Cette notion a ensuite été l’ob-
jet de nombreux travaux depuis comme par exemple [FG93, RS99, FG01] dont le but est
de proposer différentes notions de non-interférence en utilisant le formalisme d’algèbre de
processus CSP. Dans ces travaux, chaque notion dépend des hypothèses qui sont faite sur
la capacité d’observation de l’attaquant et le type d’information secrète.
Dans [BKMR08], les auteurs étendent aux systèmes de transitions la propriété d’opa-
cité introduite dans [Maz04] dans le cadre des protocoles cryptographique modélisés par
des systèmmes de réecriture. Ils montrent alors que l’opacité est une propriété suffisam-
ment générale pour pouvoir exprimer un ensemble non-négligeable d’autres propriétés de
confidentialité telles que la non-interférence (SNNI) ou encore l’anonymat [SS96]. Cette
notion d’opacité est le point de départ de ce travail de thèse et est définie par rapport à
un attaquant qui a une pleine connaissance de la structure du système et qui en observe
partiellement les exécutions. Nous définissons maintenant la propriété d’opacité.
Définition de l’opacité
Considérons un alphabet d’événements et un ensemble d’états S. Ces ensembles et
1 n
S peuvent être infinis. L’ensemble des exécutions de la forme s ! s :::s ! s qui0 1 n 1 n
peuvent être construites à partir de etS en alternant les états et les événements est noté
E( ;S) =S( S) . Considérons un système critique modélisé par le LTSM = ( ;S;;S )0
oùS dénote les états initiaux et : S!P(S) est la fonction de transition. L’ensemble0
des exécutions possibles de M est notéR(M) E( ;S) et le langage généré par M est
notéL(M) = tr(R(M)) où tr est l’opérateur qui donne la trace d’une exécution, c’est à
dire la séquence d’événements apparaissant dans cette exécution.
L’information secrète est donnée par un prédicat défini sur l’ensemble E( ;S). Plus
précisément, l’occurrence d’un run de M qui satisfait le prédicat constitue l’information
qu’un attaquant ne doit pas pouvoir inférer. Considérons maintenant que l’observation
de l’attaquant est définie par une fonction obs : E( ;S)!O oùO est l’ensemble des
observations possibles. L’architecture que nous considérons est représentée sur la figure 0.1
obs
Système M AttaquantA
Fig. 0.1: Architecture Générale pour l’opacité
On dit alors que le système M est -opaque pour obs si pour toute exécution de M qui
satisfait , il existe une autre exécution donnant la même observation et qui ne satisfait
9Contents
pas le prédicat . En d’autre terme :
0 18r2R(M); rj= =) 9r 2obs (obs(r))\R(M); r6j= (0.1)
0Dans ce cas, l’attaquant observantobs(r) ne pouvant deviner sir our a été exécuté, il ne
peut inférer si le prédicat a été satisfait par celle réellement exécutée par M.
Example 0.1 Considérons le LTS M représenté par la figure 0.2 avec =fh;;a;bg.
L’attaquant n’observe pas les états, mais observe les événements a et b. Le prédicat
est satisfait pour les runs qui contiennent l’événement h. Sur cet example, le seul run
b
a
h

a
Fig. 0.2: Un exemple de non opacité
qui explique l’observation b contient l’événement h. L’attaquant peut donc inférer pour
l’observation b que le prédicat est satisfait.
Nous allons nous intéresser dans la section suivante au problème de vérifier si un système
est opaque.
Vérification de l’opacité
Nous faisons pour cette partie quelques hypothèses supplémentaires sur la fonction d’ob-
servation et sur le type de prédicat . Tout d’abord, nous supposons que l’attaquant
observe un sous-ensemble des événements de . Nous définissons alors la projectiona
: ! qui enlève d’un mot de l’ensemble des événements qui n’appartiennenta a
pas à , c’est à dire, ceux qui ne sont pas observable par l’attaquant. La fonction d’ob-a
servation est alors donnée par la fonction p : E( ;S)! définie par p = tr.a a aa
Ensuite, nous considérons le cas d’un prédicat défini par l’accessibilité d’un ensemble
d’état F ()S.
Un moniteur pour est une fonction : !ftrue; ?g qui détermine si la satisfaction a
de par l’exécution courante deM peut être déterminée de façon sûre. Ainsi, le moniteur
doit être correct dans le sens où il ne donne pas de faux verdict. La notion de correction
10