Formalisation de propriétés de sécurité pour la protection des systèmes d'exploitation, Security properties formalization for operating system protection

Jonathan Rouzaud-Cornabas

Description

Sous la direction de Christian Toinard
Thèse soutenue le 02 décembre 2010: Orléans
Cette thèse traite du problème d’une protection en profondeur qui puisse être assurée par un système d’exploitation. Elle établit la faiblesse des solutions existantes pour l’expression des besoins de sécurité. Les approches supportent en général une seule propriété de sécurité. Nous proposons donc un langage qui permet de formaliser un large ensemble de propriétés de sécurité. Ce langage exprime les activités système directes et transitives. Il permet de formaliser la majorité des propriétés de confidentialité et d’intégrité de la littérature. Il est adapté à l’expression de modèles de protection dynamique. A titre d’exemple, un nouveau modèle dynamique est proposé pour la protection des différents domaines d’usage d’un navigateur Web. Nous définissons une méthode de compilation du langage pour analyser les appels systèmes réalisés par les processus utilisateurs. La compilation repose sur la construction et l’analyse d’un graphe de flux d’information. Nous montrons qu’en pratique la complexité reste faible. Une implantation de ce langage est proposée sous la forme d’un contrôle d’accès mandataire dynamique pour Linux. Une expérimentation à large échelle a été réalisée sur des pots-de-miel à haute interaction. Notre protection a montré son efficacité aussi bien pour les serveurs que les postes client. Il présente des perspectives intéressantes aussi bien pour la protection des systèmes que pour l’analyse de vulnérabilités. Ce travail a contribué au projet SPACLik vainqueur du défi sécurité de l’ANR SEC&SI.
-Propriétés de sécurité
The subject of this thesis is to propose an in-depth protection that can be enforced by the operating system. First, we present that current security solutions are weak in the expression of security. Indeed, most of them support only one security properties. We introduce a language that allows to formalize a large set of security properties. This language expresses directs and transitives system activities. It allows to formalize the majority of integrity and confidentiality security properties introduced in the litterature. Moreover, the language can also expresses dynamic security properties. We introduces a new dynamic security model for the protection of multiple security domains managed by a web browser. We define a method to compil our language. The purpose is to analyze the system call done by the users processes. The compilation process build and analyze an information flow graph. Futhermore, we show that the complexity of our protection solution is low. We propose an implementation of this language as a dynamic mandatory access control for Linux. We experiment it on large scale high interaction honeypots. Our protection shows its efficiency both for clients and servers. Moreover, it presents interesting perspectives for the protection of other systems and for the vulnerability analysis. This work has contributed to the SPACLik project that wins the security contest of the French National Research Agency : ANR SEC&SI.
-Security properties
Source: http://www.theses.fr/2010ORLE2075/document

Informations

• Publié par: Thesee
• Nombre de lectures: 30
• Langue: Français
• Poids de l'ouvrage: 2 Mo

Extrait

UNIVERSITÉD’ORLÉANS
ÉCOLEDOCTORALESCIENCESETTECHNOLOGIES
LABORATOIRE :LIFO
THÈSE présentéepar:
JonathanROUZAUD-CORNABAS
soutenuele:02Décembre2010
pourobtenirlegradede:Docteurdel’universitéd’Orléans
Discipline:Informatique
Formalisationdepropriétésdesécuritépourla
protectiondessystèmesd’exploitation
THÈSE DIRIGÉE PAR:
ChristianTOINARD Professeur,LIFO(Directeur)
PatriceCLEMENTE Maître de Conférences, LIFO (Co-
Responsable)
RAPPORTEURS:
FrancineKRIEF Professeur,LaBRI
Jean-YvesMARION Prof,LORIA
JURY:
MathieuBLANC Docteur,CEA-DAM
PatriceCLEMENTE MaîtredeConférences,ENSIdeBourges
FrancineKRIEF Professeur,ENSEIRB
SébastienLIMET Prof,Universitéd’Orléans
Jean-YvesMARION Professeur,EcoledesMinesdeNancy
ChristianTOINARD Professeur,ENSIdeBourges
tel-00623075, version 1 - 13 Sep 2011tel-00623075, version 1 - 13 Sep 2011Remerciements
Je remercie Mme. Francine Krief et M. Jean-Yves Marion pour avoir accepté d’évaluer mes
travaux en étant rapporteurs de cette thèse. Je tiens à remercier les membres de mon jury de thèse
dedoctorat, M.Mathieu Blanc,M.LaurentClevyetM.Sébastien Limet.
Je tiens à remercier mon directeur de thèse, M. Christian Toinard et M. Patrice Clemente,
mon co-responsable, pour leur soutien et leur aide durant la durée de mes recherches et m’avoir
offert la possibilité de réaliser cette thèse, mais aussi la région Centre et le LIFO pour avoir fi-
nancé cette thèse et m’avoir ainsi permis de réaliser ces travaux de recherche. Je tiens également
à remercier M. Jeremy Briffaut pour son aide et son soutien tout au long de ma thèse. Je tiens àtouslesmembresdel’équipeSécuritéetDistributiondesSystème,M.PascalBerthome,
M. Jean-François Lalande et M. Yacine Zémali, ainsi que M. Martial Szpieg professeur à l’ENSI
deBourges,pourlesnombreusesdiscussionsenrichissantesetpourtoutel’aidequ’ilsm’ontfourni
durant cette thèse. Je remercie aussi l’ENSI de Bourges pour m’avoir accueilli dans ses locaux et
m’avoiroffert un cadre agréable de travail.
Je voudrais remercier mes amis, ma famille pour leurs encouragements et leur soutien et sur-
tout ma femme Stéphanie Ollier pour ses nombreuses relectures et son soutien tout au long de ma
thèse.
tel-00623075, version 1 - 13 Sep 20114
tel-00623075, version 1 - 13 Sep 2011Table des mati res
1 Introduction 15
2 État de l’art 19
2.1 Politique de sécurité . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
2.1.1 Politique de sécurité . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
2.1.2 Propriétés degénérales . . . . . . . . . . . . . . . . . . . . . . 21
2.1.3 de sécuritédérivées . . . . . . . . . . . . . . . . . . . . . . . 23
2.1.4 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
2.2 Modèles de Protection . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
2.2.1 Contrôle d’accès discrétionnaire . . . . . . . . . . . . . . . . . . . . . . 25
2.2.2 mandataire . . . . . . . . . . . . . . . . . . . . . . . . 27
2.3 Protection systèmeorientéeobjectifs de sécurité . . . . . . . . . . . . . . . . . . 33
2.3.1 Modélisation parautomates . . . . . . . . . . . . . . . . . . . . . . . . 33
2.3.2 Intégrité etConfidentialité . . . . . . . . . . . . . . . . . . . . . . . . . 34
2.3.3 Contrôle de fluxd’information . . . . . . . . . . . . . . . . . . . . . . . 36
2.3.4 Abus de privilèges . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
2.3.5 Séparation de privilèges . . . . . . . . . . . . . . . . . . . . . . . . . . 40
2.3.6 Situation de concurrence . . . . . . . . . . . . . . . . . . . . . . . . . . 41
2.4 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
3 Langage de formalisation des activités 45
3.1 Entités du Système d’Exploitation etOpérations . . . . . . . . . . . . . . . . . . 45
3.1.1 Contexte desécurité . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
3.1.2 Opération Élémentaire . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
3.1.3 Datation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
3.1.4 Événements etDatation . . . . . . . . . . . . . . . . . . . . . . . . . . 48
3.2 ActionÉlémentaire . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
3.2.1 Interaction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
3.2.2 Estampillée . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
3.2.3 Traces . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
3.2.4 Flux d’InformationDirect . . . . . . . . . . . . . . . . . . . . . . . . . 53
3.2.5 FluxDirectEstampillé . . . . . . . . . . . . . . . . . . . 54
3.2.6 FluxDirectMultiple . . . . . . . . . . . . . . . . . . . . 54
3.2.7 Flux d’InformationDirectGénéral . . . . . . . . . . . . . . . . . . . . . 56
3.3 Flux d’Information Indirect . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
3.3.1 Relation de dépendancecausale . . . . . . . . . . . . . . . . . . . . . . 56
3.3.2 Définition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
3.4 Flux d’Information Général . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
3.5 Langagede description d’activités . . . . . . . . . . . . . . . . . . . . . . . . . 61
5
tel-00623075, version 1 - 13 Sep 20116 TABLEDESMATIÈRES
4 Formalisation de Propriétés de Sécurité 63
4.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
4.2 Exécution parTransition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
4.2.1 Exécution Indirecte . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
4.2.2 Générale . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
4.3 Intégrité . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
4.3.1 Intégrité des Objets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
4.3.2 des Sujets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67
4.3.3 Intégrité Générale . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68
4.3.4 Situation de Concurrence . . . . . . . . . . . . . . . . . . . . . . . . . . 70
4.3.5 Intégrité des Domaines . . . . . . . . . . . . . . . . . . . . . . . . . . . 70
4.3.6 Executablede Confiance . . . . . . . . . . . . . . . . . . . . . . . . . . 73
4.4 Confidentialité . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76
4.4.1 Confidentialité des Données . . . . . . . . . . . . . . . . . . . . . . . . 76
4.5 MultiLevelSecurity (MLS) . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
4.5.1 Bell&LaPadulaRestrictifavecPlage . . . . . . . . . . . . . . . . . . . . 78
4.5.2 Extensions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79
4.6 Abus de privilèges . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81
4.6.1 Séparation de Privilèges . . . . . . . . . . . . . . . . . . . . . . . . . . 81
4.6.2 Absence de ChangementdeContexte . . . . . . . . . . . . . . . . . . . 81
4.6.3 Respect d’une Politique . . . . . . . . . . . . . . . . . . . . . . . . . . 82
4.7 Propriétés Dynamique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84
4.7.1 Muraille de Chine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84
4.7.2 Confinement des Données à la Volée : Un nouveau modèle de protection
dynamique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86
4.8 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93
5 Implantation du langage 95
5.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95
5.2 Graphe d’Interactions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95
5.3 Graphes de Fluxd’Information . . . . . . . . . . . . . . . . . . . . . . . . . . . 95
5.3.1 Graphe de Fluxd’Information . . . . . . . . . . . . . . . . . . . . . . . 96
5.3.2 de FluxAugmenté . . . . . . . . . . . . . . . . . 97
5.3.3 Complexité des différents graphes . . . . . . . . . . . . . . . . . . . . . 98
5.4 Miseen oeuvre des opérateurs . . . . . . . . . . . . . . . . . . . . . . . . . . . 100
5.4.1 Fluxd’Information Direct . . . . . . . . . . . . . . . . . . . . . . . . . 100
5.4.2 Cherche un Fluxd’InformationIndirect . . . . . . . . . . . . . . . . . . 101
5.4.3 Tous les Flux Indirects . . . . . . . . . . . . . . 103
5.4.4 FluxGénéral . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104
5.5 Compilationdu langage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104
5.5.1 Méthode générique pourlacompilation denotrelangage . . . . . . . . . 104
5.5.2 Exemples de Propriétés deSécurité . . . . . . . . . . . .