Monitoring and Supervisory Control for Opacity

profil-zyak-2012 - Roland Groz

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

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

161 pages

Français

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

A propos
Informations
Extrait

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

Darondeau

Institut polytechnique de Grenoble

Université européenne de Bretagne

Rennes

Fourier

Raskin

Property

Université de Rennes

Université Libre de Bruxelles

Marchand

Abstract interpretation

Informations

Publié par	profil-zyak-2012
Nombre de lectures	59
Langue	Français
Poids de l'ouvrage	1 Mo

Extrait

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 ﬁl de nos collaborations, a beaucoup inﬂuencé 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 eﬀet 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 Conﬁdential Information and Notion of Attackers . . . . . . . . . . . . . . . 51
3.2 Deﬁnition 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 ﬁables et eﬃcaces pour certiﬁer la sécurité
d’un système est essentiel. Aﬁn d’étudier de tels algorithmes de certiﬁcation, les propriétés
de sécurité sont généralement classiﬁées en trois catégories :
– l’intégrité;
– la disponibilité;
– la conﬁdentialité.
Une politique de sécurité consiste en un ensemble de propriétés de sécurité, de diﬀérentes
catégories,quidoiventêtreconjointementsatisfaitessurlesystème.Nousdonnonsquelques
explicationssurchacunedecescatégoriesaﬁndesituerdansquelcadreseplacenostravaux
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 conﬁguration critique. Si l’on choisit comme
exemple un système de vote, le fait que personne ne puisse modiﬁer 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ériﬁer 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 conﬁdentialité sont celles qui no