173 Pages
English

Réécriture et modularité pour les politiques de sécurité, Rewriting and modularity for security policies

-

Gain access to the library to view online
Learn more

Description

Sous la direction de Claude Kirchner, Hélène Kirchner
Thèse soutenue le 31 mars 2008: Nancy 1
Dans cette thèse, nous nous intéressons à la spécification et à l’analyse modulaires de politiques de sécurité flexibles basées sur des règles. Nous introduisons l’utilisation du formalisme de réécriture stratégique dans ce domaine, afin que notre cadre hérite des techniques, des théorèmes, et des outils de la théorie de réécriture. Ceci nous permet d’énoncer facilement et de vérifier des propriétés importantes des politiques de sécurité telles que l’absence des conflits. En outre, nous développons des méthodes basées sur la réécriture de termes pour vérifier des propriétés plus élaborées des politiques. Ces propriétés sont la sûreté dans le contrôle d’accès et la détection des flux d’information dans des politiques obligatoires. Par ailleurs, nous montrons que les stratégies de réécriture sont importantes pour préserver des propriétés des politiques par composition. Les langages de stratégies disponibles dans des systèmes comme Tom, Stratego, Maude, ASF+SDF et Elan, nous permettent de définir plusieurs genres de combinateurs de politiques. Enfin, nous fournissons également une méthodologie pour imposer à des applications existantes, de respecter des politiques basées sur la réécriture via la programmation par aspects. Les politiques sont tissées dans le code existant, ce qui génère des programmes mettant en oeuvre des moniteurs de référence. La réutilisation des politiques et des programmes est améliorée car ils peuvent être maintenus indépendamment.
-Politiques de Sécurité
In this thesis we address the modular specification and analysis of flexible, rule-based policies. We introduce the use of the strategic rewriting formalism in this domain, such that our framework inherits techniques, theorems, and tools from the rewriting theory. This allows us to easily state and verify important policy properties such as the absence of conflicts, for instance. Moreover, we develop rewrite-based methods to verify elaborate policy properties such as the safety problem in access control and the detection of information flows in mandatory policies. We show that strategies are important to preserve policy properties under composition. The rich strategy languages available in systems like Tom, Stratego, Maude, ASF+SDF and Elan allows us to define several kinds of policy combiners. Finally, in this thesis we provide a systematic methodology to enforce rewrite-based policies on existing applications through aspect-oriented programming. Policies are weaved into the existing code, resulting in programs that implement a reference monitor for the given policy. Reuse is improved since policies and programs can be maintained independently from each other.
Source: http://www.theses.fr/2008NAN10007/document

Subjects

Informations

Published by
Reads 24
Language English
Document size 1 MB




AVERTISSEMENT

Ce document est le fruit d'un long travail approuvé par le
jury de soutenance et mis à disposition de l'ensemble de la
communauté universitaire élargie.

Il est soumis à la propriété intellectuelle de l'auteur. Ceci
implique une obligation de citation et de référencement lors
de l’utilisation de ce document.

Toute contrefaçon, plagiat, reproduction illicite encourt une
poursuite pénale.


➢ Contact SCD Nancy 1 : theses.sciences@scd.uhp-nancy.fr




LIENS


Code de la Propriété Intellectuelle. articles L 122. 4
Code de la Propriété Intellectuelle. articles L 335.2- L 335.10
http://www.cfcopies.com/V2/leg/leg_droi.php
http://www.culture.gouv.fr/culture/infos-pratiques/droits/protection.htm D´epartement de formation doctorale en informatique
´Ecole doctorale IAEM Lorraine
R´e´ecriture et Modularit´e pour les
Politiques de S´ecurit´e
`THESE
pr´esent´ee et soutenue publiquement le 31 Mars 2008
pour l’obtention du
Doctorat de l’Universit´e Henri Poincar´e
(sp´ecialit´e informatique)
par
Anderson Santana de Oliveira
Composition du jury
Rapporteurs : Fr´ed´eric Cuppens Professeur, ENST-Bretagne, Rennes, France
Maribel Fernandez Professeur, King’s College London, Londres, Royaume-Uni
Examinateurs : Piero A. Bonatti Professeur, Universit`a di Napoli Federico II, Naples, Italie
Isabelle Chrisment Professeur,´e Henri Poincar´e , Nancy, France
Daniel J. Dougherty Professeur, Worcester Polytechnic Institute, Worcester, MA, USA
Th´er`ese Hardin Professeur, Universit´e Paris VI, Paris, France
Claude Kirchner Directeur de recherche, INRIA, Bordeaux, France
H´el`ene Kirchner Directeur de re, INRIA, Bordeaux, France
Laboratoire Lorrain de Recherche en Informatique et ses Applications — UMR 7503Remerciements
Je remercie Claude et Hélène Kirchner qui m’ont fait l’honneur de diriger ma thèse avec une
granderigueurscientifiqueetquim’ontsoutenuavecenthousiasmetoutaulongdecetravail.Je
tiensàleurexprimermaprofondegratitude.
Je remercie vivement les membres du jury : Frédéric Cuppens et Maribel Fernandez qui ont
eulagentillessederapportersurcettethèse;ThérèseHardinlaprésidentedujury;PieroBonatti
quim’afaitdescommentairestrèsconstructifsdèsnotrepremiercontactlorsdemaprésentation
àlaréunionannuelleduréseaud’excellenceRewerseen2006;IsabelleChrismentqui,avecses
questionspertinentes,m’aaidéàjustifiermadémarche;etDanDoughertyquim’achaleureuse
mentaccueilliauseindudépartementd’informatiqueduWorcesterPolytechnicInstituteetavec
quij’aieuleplaisirdetravailler.
Merci également aux participants du Projet ANR SSURF avec qui j’ai eu des discussions
fructueuses,enparticulierCharlesMorissetpournotrecollaboration.
Cette thèse n’aurait jamais été ce qu’elle est aujourd’hui sans mes échanges scientifiques
importants avec les membres de l’équipe PROTHEO et PAREO. Je tiens à remercier Horatiu
Cirstea et Pierre Etienne Moreau pour l’intérêt qu’ils ont manifesté à l’égard de cette thèse et
pourleursremarquespertinentes.MesremerciementsvontégalementàYohanBoichutquis’est
penché à mes côtés sur le problème de l’indécidabilité de la propriété de sûreté dans le modèle
HRU.
Je remercie tous les stagiaires avec qui j’ai travaillé : tout particulièrement, Eric Ke Wang,
ainsiqueSelinaZhenWangetChristopheMassonquiontchacunapportéleurpierreàl’édifice.
Merci à tous les thésards de l’équipe PROTHEO, particulièrement Oana Andrei pour son
amitié, et mes anciens collègues de bureau Colin Riba, Laura Lowenthal et Tony Bourdier pour
leurgentillesse.
Je remercie la CAPES et l’INRIA pour leur confiance et la bourse qu’ils m’ont accordées.
J’adresse également mes remerciements au personnel de l’Université Henri Poincaré et du LO
RIA qui ont contribué efficacement au bon déroulement de ma thèse, principalement Chantal
Llorenspoursonincroyablepatienceetsabonnehumeur.
Enfin je remercie mes parents, mon frère, mes soeurs, ainsi qu’Annette et Alphonse, pour
leursoutieninconditionnel.Jegardelemeilleurpourlafinenadressantunedédicacespécialeà
Marie Angequiasufairepreuved’amouretdepatience.
1Para Lourdes, Gilberto, Andreza, Elton, Hemiliane, Amanda e Marie Ange.
2Tabledesmatières
1 RésuméÉtendu 1
1.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
1.1.1 Motivations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
1.1.2 Historique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
1.2 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
1.2.1 SpécificationdePolitiquesdesécurité . . . . . . . . . . . . . . . . . . 9
1.2.2 VérificationdePropriétés . . . . . . . . . . . . . . . . . . . . . . . . 15
1.2.3 CompositiondesPolitiquesavecdesStratégiesdeRéécriture . . . . . . 18
1.2.4 ImplantationdesdeSécurité . . . . . . . . . . . . . . . . . 23
1.3 ConclusionsetPerspectives . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
1.4 PlandelaThèse . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2 Introduction 31
2.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
2.2 HistoricalBackground . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
2.3 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
2.4 OverviewoftheThesis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
3 BackgroundonRewritingandStrategies 37
3.1 PreliminaryNotions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
3.1.1 TermAlgebra . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
3.1.2 EquationalTheories . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
3.1.3 TermOrderings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
3.1.4 AbstractReductionSystems . . . . . . . . . . . . . . . . . . . . . . . 42
3.2 TermRewriting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
3.2.1 Conditionalrewriting . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
3.2.2 RewritingModuloanEquationalTheory . . . . . . . . . . . . . . . . 45
3.3 StrategicRe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
3.3.1 AbstractStrategies . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
3.3.2 PropertiesunderStrategies . . . . . . . . . . . . . . . . . . . . . . . . 47
3.3.3 StrategyConstructors . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
3.4 TheTomSystem: TermRewritingSystemsinJava . . . . . . . . . . . . . . . 49
4 PolicySpecification 53
4.1 StateoftheArt . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
4.2 ARewrite BasedFramework . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
3Tabledesmatières
4.3 PolicyProperties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
4.4 DecidableClasses . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70
4.5 RelatingDatalogandTermRewriting . . . . . . . . . . . . . . . . . . . . . . 72
4.6 RelatedWorks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
4.7 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82
5 PolicyVerification 83
5.1 VerifyingInformationFlowPolicies . . . . . . . . . . . . . . . . . . . . . . . 83
5.1.1 TheBellandLaPadulaModel . . . . . . . . . . . . . . . . . . . . . . 84
5.1.2 TheMcLeanModel. . . . . . . . . . . . . . . . . . . . . . . . . . . . 86
5.1.3 AnAnalysisAlgorithmforInformationFlow . . . . . . . . . . . . . . 89
5.2 CheckingSafetyinRewriting BasedPolicies . . . . . . . . . . . . . . . . . . 92
5.2.1 TheHRUmodelasaRewriteSystem . . . . . . . . . . . . . . . . . . 94
5.2.2 VerifyingSafety . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97
5.3 RelatedWorks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 98
5.4 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99
6 PolicyComposition 101
6.1 Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102
6.2 PolicyCombiners . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 103
6.2.1 SimpleUnionofPolicyRules . . . . . . . . . . . . . . . . . . . . . . 103
6.2.2 SequentialPolicyCombination . . . . . . . . . . . . . . . . . . . . . . 105
6.2.3 ConservativePolicyExtension . . . . . . . . . . . . . . . . . . . . . . 108
6.2.4 XACML likePolicyCombiners. . . . . . . . . . . . . . . . . . . . . . 109
6.3 RelatedWorks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114
6.4 ConclusionsandFutureWorks . . . . . . . . . . . . . . . . . . . . . . . . . . 116
7 PolicyEnforcement 119
7.1 TheRunningExample . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 120
7.2 PoliciesinTom . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 121
7.3 EnforcingRewrite BasedAccessControl . . . . . . . . . . . . . . . . . . . . 122
7.3.1 Aspect OrientedProgramming . . . . . . . . . . . . . . . . . . . . . . 124
7.3.2 SystemArchitecture . . . . . . . . . . . . . . . . . . . . . . . . . . . 124
7.3.3 AspectsforAccessControl . . . . . . . . . . . . . . . . . . . . . . . . 125
7.4 RelatedWorks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 128
7.5 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 129
8 ConclusionsandPerspectives 131
8.1 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 131
8.2 FuturePerspectives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 132
4Tabledesmatières
A PolicyImplementationswithTom 135
A.1 VeficationofInformationFlowinMACmodels . . . . . . . . . . . . . . . . . 135
A.1.1 TheMcLean’spolicyimplementation . . . . . . . . . . . . . . . . . . 135
A.1.2 Theimplementationoftheverificationalgorithm . . . . . . . . . . . . 136
A.2 ARewrite BasedImplementationoftheHRUModel . . . . . . . . . . . . . . 139
A.3 APolicyCompositionAlgebrainTom . . . . . . . . . . . . . . . . . . . . . . 144
A.4 TheConferencePolicyinTom . . . . . . . . . . . . . . . . . . . . . . . . . . 145
A.5 AspectJCodefortheConferenceSystem . . . . . . . . . . . . . . . . . . . . 148
Bibliography 151
5Tabledesmatières
6Chapitre1
RésuméÉtendu
1.1 Introduction
Ce chapitre présente un résumé en langue française des principales contributions de cette
thèse.Salecturepourraêtreeffectuéedefaçonindépendantedurestantdudocumentenanglais,
àl’exceptiondesdéfinitionsformellessurlaréécritureavecdesstratégies,donnéesdansleCha
pitre 3. Ce chapitre apporte une compréhension de l’ensemble des enjeux autour des politiques
de sécurité, de leur composition et de la manière dont ces problèmes sont abordés dans nos
travaux.
Ce chapitre expose d’abord les motivations des travaux de recherche réalisés pendant cette
thèse dans la Section 1.1.1. Ensuite, nous présentons l’historique de la recherche dans le do
mainedelaspécificationformelledepolitiquesdesécuritédanslaSection1.1.2.LaSection1.2
présente les principaux résultats obtenus dans cette thèse. La section 1.3 présente des conclu
sions et montre quelques directions futures de recherche. La 1.4 un panorama
surlerestantdecemanuscritdethèse.
1.1.1 Motivations
À l’âge de l’information, l’économie, les communications et les divertissements dépendent
des ordinateurs. Des informations d’une valeur inestimable pour beaucoup d’agents (compa
gnies, gouvernements, etc.) circulent dans des systèmes d’information de grande taille, souvent
reliésenréseauàd’autressystèmes.Danscecontexte,unproblèmeprimordialtraitéparlespo
litiques de sécurité est la protection des données gérées par ces systèmes contre des utilisations
indésirables. Selon Bishop [Bishop,2004], une politique de sécurité est une déclaration de ce
quiestpermisetdecequinel’estpas.Cespolitiquessontdoncdesspécificationsextrêmement
importantes,danslamesureoùlasécuritéd’unequantitéénormed’informationsmanipuléespar
des ordinateurs (ou de façon plus abstraite, des ressources) dépendent de la formulation claire
desexigencesdesécurité.
Les e de sécurité déterminent les situations dans lesquelles un système peut être ex
posé à desattaques : (i) des informations secrètespeuvent être révélées à desagents qui ne sont
pas censés l’obtenir, (ii) des peuvent être corrompues ou modifiées de façon telle
qu’on ne peut plus avoir confiance en son contenu, ou encore détruites et (iii) des informations
peuvent être retenues et devenir indisponibles pendant un intervalle de temps crucial. Ces trois
pointssontappeléesrespectivementdeconfidentialité,intégritéetdisponibilité.Unepolitiquede
sécurité se concentre habituellement sur un de ces aspects, mais son but dans une configuration
1