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

Anderson Santana De Oliveira

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

Informations

• Publié par: Thesee
• Nombre de lectures: 24
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

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 : [e-mail]




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