<figure><img src="image_1.png" /></figure>

HAL
open science

# Descriptions formelles : Comprendre, Corriger, Implanter, Résutiliser. Application au contrôle d'accès

Mathieu Jaume

► To cite this version:

Mathieu Jaume. Descriptions formelles : Comprendre, Corriger, Implanter, Résutiliser. Application au contrôle d'accès. Informatique [cs]. Pierre et Marie Curie, Paris VI, 2008. tel-04273170

HAL Id: tel-04273170

https://hal.science/tel-04273170

Submitted on 7 Nov 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

Public Domain
UNIVERSITÉ PIERRE ET MARIE CURIE – PARIS 6

HABILITATION À DIRIGER DES RECHERCHES

Spécialité : INFORMATIQUE

présentée par :

Mathieu JAUME

# Descriptions formelles :
Comprendre, Corriger, Implanter, Réutiliser

## Application au contrôle d'accès

Soutenue le 06 Novembre 2008 devant le jury composé de :

## Rapporteurs

<table><tr><td>Hélène KIRCHNER</td><td>Directrice de Recherche</td><td>INRIA Bordeaux, France</td></tr><tr><td>César A. MUÑOZ</td><td>Senior Scientist</td><td>National Institute of Aerospace, USA</td></tr><tr><td>Luca VIGANÒ</td><td>Professeur</td><td>Università di Verona, Italie</td></tr></table>

## Examinateurs

<table><tr><td>Irène GUESSARIAN</td><td>Professeur</td><td>Université Paris 6, France</td></tr><tr><td>Thérèse HARDIN</td><td>Professeur</td><td>Université Paris 6, France</td></tr><tr><td>Ludovic MÉ</td><td>Professeur</td><td>SUPELEC Rennes, France</td></tr><tr><td>Isabelle SIMPLOT-RYL</td><td>Professeur</td><td>Université Lille 1, France</td></tr></table>
<figure><img src="image_2.png" /></figure>
A la mémoire de Ivan Evrard.
<figure><img src="image_3.png" /></figure>
Remerciements

Hélène Kirchner, César A. Muñoz et Luca Viganò ont accepté de rapporter ce document.
Je leur exprime ici toute ma gratitude pour leur lecture attentive de ce document, pour
les remarques qu'ils m'ont faites pour l'améliorer ainsi que pour les discussions que nous
avons eues.

Depuis 2001, j'ai la chance immense de travailler aux côtés de Thérèse Hardin. Son enthousiasme et sa gentillesse m'ont accompagné ces dernières années, durant lesquelles j'ai pu profiter de sa patience, de sa disponibilité, de son soutien, de son optimisme ainsi que de ses connaissances scientifiques dans de nombreux domaines. Mais je voudrais surtout remercier Thérèse pour le plaisir que j'ai à travailler dans l'équipe SPI qu'elle dirige.

Le premier cours de sémantique que j'ai suivi lorsque j'étais étudiant était celui que donnait Irène Guessarian. Je lui dois donc beaucoup pour m'avoir fait découvrir ce domaine. Irène a ensuite présidé mon jury de thèse et m'a accueilli dans son équipe pédagogique lors de mon arrivée à l'UPMC. Irène est depuis une collègue loyale et généreuse et a accepté de présider le jury de cette HDR. J'en suis très heureux.

J'ai rencontré Ludovic Mé lors de la soutenance de thèse de Charles Morisset. Son intérêt pour la sécurité et les méthodes formelles nous ont alors conduit à travailler ensemble sur la détection de flots. Je tiens bien sûr à remercier Ludovic pour sa participation à ce jury, mais aussi pour les échanges fructueux que nous avons eus.

J'adresse aussi de chaleureux remerciements à Isabelle Simplot-Ryl pour avoir consacré du temps à la lecture de ce document et je suis très honoré de sa participation au jury de cette HDR.

A l'issue de ma thèse, j'ai commencé à travailler avec Catherine Dubois. Depuis, nos chemins se croisent régulièrement et nous conduisent à collaborer sur des sujets très variés. Je tiens ici à remercier Catherine pour avoir accompagné mes activités de recherche ainsi que pour sa gentillesse et son soutien.

L'encadrement de doctorants est enrichissant à plus d'un titre et je tiens à remercier Charles Morisset (qui a soutenu sa thèse en 2007), ainsi que Lionel Habib et Lién Tran (actuellement en thèse). J'ai beaucoup appris en tentant de répondre à leurs nombreuses questions, toujours pertinentes, et les remercie pour leur confiance et leurs contributions.

L'ensemble des travaux présentés ici est bien sûr le fruit de collaborations : Véronique Delebarre, Catherine Dubois, Thérèse Hardin, Ludovic Mé, Virgile Prevosto, Valérie Viet Triem Tong ont contribué au travail présenté dans ce document et je les remercie vivement de m'avoir permis de partager avec eux mes activités de recherche.

Je tiens aussi à remercier Philippe Ayrault, Julien Blond, Matthieu Carlier, David Delahaye, Damien Doligez, Emmanuel Gureghian, Eric Jaeger, Ivan Noyer, François Pessaux, Renaud Rioboo, Véronique Viguié-Donzeau-Gouge, Pierre Weis, très proches collaborateurs de l'équipe SPI, qui par leur aide, leurs encouragements et leurs remarques m'ont permis de mener mes recherches dans un environnement stimulant. J'associe à ces remerciements l'ensemble des participants des actions Modulogic et ANR SSURF, ainsi que du PlanPluriFormation Logiciels Sûrs.
Mon goût pour les études coïncide avec ma rencontre avec Alain David. Il ne s'agit bien sûr pas d'une simple coïncidence, et je tiens à remercier Alain pour l'originalité de ses points de vue et pour son soutien depuis de très nombreuses années maintenant.

Kevin Adoua a toujours su m'accompagner dans mes démarches administratives. Je le remercie pour son efficacité et sa gentillesse.

Je souhaite aussi remercier mes parents pour m'avoir les premiers appris à apprendre et pour leurs encouragements. Enfin, je remercie Areski, Caroline, James, Luc, Mark, Myriam, Olivier, Philippe et Sylvie qui avec beaucoup de délicatesse, de chaleur, de rires et de sourires me rendent la vie si douce et si joyeuse.
# Table des matières

<table><tr><td>Introduction</td><td>1</td></tr><tr><td>1 Développements formels</td><td>5</td></tr><tr><td>1.1 Formalisations</td><td>6</td></tr><tr><td>1.1.1 Unification et SLD-résolution</td><td>6</td></tr><tr><td>1.1.2 Modèles de contrôles d'accès</td><td>8</td></tr><tr><td>1.2 Réutilisation de développements formels</td><td>16</td></tr><tr><td>1.2.1 Ingénierie de la preuve</td><td>16</td></tr><tr><td>1.2.2 Définition de cadres génériques</td><td>18</td></tr><tr><td>2 Contrôler le contrôle d'accès</td><td>20</td></tr><tr><td>2.1 Un cadre sémantique pour la définition de modèles de contrôle d'accès</td><td>21</td></tr><tr><td>2.1.1 Politiques de contrôle d'accès</td><td>22</td></tr><tr><td>2.1.2 Modèles de contrôle d'accès</td><td>24</td></tr><tr><td>2.2 Comparaison de modèles de contrôle d'accès</td><td>26</td></tr><tr><td>2.2.1 Comparaison de modèles : Accès</td><td>26</td></tr><tr><td>2.2.2 Comparaison de modèles : Administration</td><td>29</td></tr><tr><td>2.3 Analyse de flots d'information</td><td>32</td></tr><tr><td>2.3.1 Flots et Politiques de Flots</td><td>32</td></tr><tr><td>2.3.2 Mécanismes de détection de flots</td><td>35</td></tr><tr><td>2.4 Analyse de modèles de contrôle d'accès</td><td>36</td></tr><tr><td>Conclusion</td><td>39</td></tr><tr><td>A L'atelier Focal</td><td>49</td></tr><tr><td>B Formalisations</td><td>52</td></tr><tr><td>B.1 Unification des termes du premier ordre</td><td>52</td></tr><tr><td>B.1.1 Formalisation de l'unification dans le système Coq</td><td>52</td></tr><tr><td>B.1.2 Formaliser ce qui semble déjà formel?</td><td>53</td></tr><tr><td>B.2 Sémantique de la programmation logique</td><td>55</td></tr><tr><td>B.2.1 Plongement profond : Formaliser pour corriger</td><td>56</td></tr><tr><td>B.2.2 Plongement superficiel : Formaliser pour mieux comprendre</td><td>62</td></tr></table>
<table><thead><tr><th></th><th></th><th></th></tr></thead><tbody><tr><td>C</td><td>Pratique des méthodes formelles</td><td>69</td></tr><tr><td>C.1</td><td>Changement de représentation</td><td>69</td></tr><tr><td>C.1.1</td><td>Réutilisation de preuves : définition d'isomorphismes au sein du langage de spécification</td><td>69</td></tr><tr><td>C.1.2</td><td>Réutilisation de preuves : Outil externe de transformation de preuves</td><td>72</td></tr><tr><td>C.1.3</td><td>Preuves dans un architecture hiérarchique</td><td>77</td></tr><tr><td>C.2</td><td>Un cadre générique pour la spécification de formalismes logiques</td><td>80</td></tr><tr><td>C.2.1</td><td>Spécification d'un cadre générique</td><td>80</td></tr><tr><td>C.2.2</td><td>Instanciations</td><td>82</td></tr><tr><td>D</td><td>Contrôle d'accès</td><td>85</td></tr><tr><td>D.1</td><td>Modèles de contrôle d'accès</td><td>85</td></tr><tr><td>D.1.1</td><td>Exemples de Politiques de contrôle d'accès</td><td>85</td></tr><tr><td>D.1.2</td><td>Modèles et implantations</td><td>87</td></tr><tr><td>D.2</td><td>Comparaison de modèles de contrôle d'accès</td><td>90</td></tr><tr><td>D.2.1</td><td>Simulation d'implantations</td><td>90</td></tr><tr><td>D.2.2</td><td>Simulation faible d'implantations</td><td>96</td></tr><tr><td>D.3</td><td>Analyse de flots</td><td>102</td></tr><tr><td>D.3.1</td><td>Flots engendrés par les exécutions d'un moniteur de référence</td><td>102</td></tr><tr><td>D.3.2</td><td>Mécanisme de détection de flots</td><td>102</td></tr><tr><td>D.3.3</td><td>Application</td><td>104</td></tr></tbody></table>
# Introduction

## Des détails qui n'en sont pas

Comme dans toutes les autres disciplines scientifiques, le besoin de recourir à des mo-dèles et formalismes mathématiques se fait ressentir en informatique, pour mieux com-prendre et analyser les problèmes traités par cette science. C'est de ce besoin que viennent les méthodes dites "formelles". Dans [4], P. Amey définit la "chose" formelle comme une "cho-se" soutenue par une rigueur mathématique. Effectivement, les méthodes formelles peuvent être définies comme des méthodes soutenues par une rigueur mathématique, et peut-être plus exactement, comme des méthodes s'appuyant fortement sur une (ou des) branche(s) des mathématiques. Leur utilité première est leur imperméabilité à toute ambiguïté. Cela est très apprécié lorsqu'il s'agit de spécifier (décrire ce qui est requis d'un système) ou encore lorsqu'il s'agit de développer (architecture, code). De plus, elles permettent très naturellement de démontrer le respect de certaines propriétés et donc, d'augmenter la confiance dans le système, que ce soit sur la cohérence de sa spécification ou sur la bonne adéquation de son développement à cette spécification. Lorsqu'il s'agit de systèmes logiciels critiques, ces propriétés peuvent être vitales.

Le besoin de confiance est déjà fortement ressenti pour les "outils de base" de l'infor-matique comme les algorithmes classiques. Plus qu'une simple vérification, la spécification formelle de tels outils et la formalisation des preuves de leurs propriétés permettent bien sûr d'accroître la fiabilité de leur implémentation. Mais elles permettent souvent de mettre en lumière certains points délicats et donc sources d'erreurs ou de confusions, que le "monde informel" ignore volontairement par souci de "lisibilité". Ces points délicats sont souvent injustement qualifiés de "détails". Selon le dictionnaire de l'Académie Française, le mot "dé-tail" peut désigner un élément accessoire, un fait secondaire sur lequel on passe légèrement, un point de peu d'importance ou encore un élément négligeable. La pratique des méthodes formelles conduit donc à se pencher sur des détails qui de fait n'en sont pas ... et si la présentation des travaux issus de cette pratique est rarement spectaculaire, les problèmes qu'elle permettrait d'éviter peuvent parfois l'être :

- En 1996, le vol inaugural du lanceur européen Ariane 5 "crash" quelques secondes après son décollage. L'explosion, due à une erreur logicielle (non respect d'une contrainte de domaine) a coûté environ un demi milliard de dollars.

- En Novembre 2005, un bogue bloque toutes les côtations durant une journée à la bourse de Tokyo.

- En Octobre 2007, un canon anti-aérien Oerlikon de l'armée Sud-Africaine s'est re-tourné, tout en tirant, au hasard, faisant 9 morts et 14 blessés. Le logiciel est en cause dans cet incident.
- Le 13 Novembre 2007 au soir, 10000 sites web hébergés par Ovh, premier hébergeur français, connaissent des difficultés. En effet, Ovh subit un “crash” majeur sur un des 16 serveurs de stockage. Les sites ont été inaccessibles (erreur 404) une vingtaine d’heures environ et les données ajoutées durant les 7 derniers mois dans les CMS par les utilisateurs ont été définitivement perdues.

Cette liste n’est évidemment pas exhaustive et une étude menée par le *National Institute of Standards and Technology* évalue à 60 milliards de dollars par an le coût des bogues informatiques. Rappelons qu’il est souvent considéré que les éditeurs de logiciels consacrent environ 80% de leurs dépenses à identifier et à corriger des erreurs de logiciel, mais cela ne suffit pas à empêcher la multiplication des bogues.

Les méthodes formelles reposent sur l'utilisation d'outils mathématiques pour spécifier et valider les systèmes informatiques. Le recours à ces outils est justifié par le besoin de rigueur et de précision dans la description du comportement de systèmes complexes, et par la nécessité de disposer de mécanismes d'abstraction afin de juguler cette complexité. Les travaux présentés dans ce document illustrent la mise en œuvre de méthodes formelles et des outils logiciels associés pour étudier des objets variés. Pour certains d'entre eux, la littérature fournit une description mathématique et il peut sembler inutile d'exprimer cette description à l'aide d'un langage formel logique. Pourtant, une lecture minutieuse de ces descriptions, nécessaire pour obtenir un développement formel, révèle l'existence de plusieurs définitions non équivalentes pour un même objet. Les différences qui apparaissent entre ces définitions sont alors parfois sources de confusions ou d'erreurs dans les preuves mais aussi dans les énoncés de résultats garantissant des propriétés sur l'objet formalisé. L'exemple le plus typique est celui de la notion de substitution. Cette opération permet de remplacer certaines variables par un terme au sein d'une expression et peut sembler à première vue simple à spécifier. Cependant, la spécification formelle de cette opération nécessite de préciser certains "détails" : s'agit-il d'une fonction totale ? d'une fonction partielle ? quelles sont les propriétés de séparation des variables apparaissant dans le domaine et dans l'image de cette fonction ? Des réponses différentes à ces questions conduisent à des définitions non équivalentes. En rassemblant des résultats établis à partir de définitions non équivalentes pour une même notion, il devient alors possible d'établir des résultats erronnés si l'on omet ces "détails". Formaliser permet donc non seulement de préciser l'objet formalisé mais aussi de corriger certaines erreurs. Bien sûr, une difficulté supplémentaire apparaît lorsque l'objet à formaliser est décrit en langage naturel. Plusieurs interprétations de cette description sont généralement possibles et il s'agit de lever les ambiguïtés et d'expliciter les hypothèses implicites. Dans ce cas, le travail de formalisation permet non seulement de corriger certaines confusions mais permet aussi d'avoir une compréhension plus fine de l'objet par sa formalisation.

Si la mise en œuvre des méthodes formelles permet de garantir les propriétés essentielles d'un algorithme, celles des mécanismes d'exécution d'un programme ou encore des propriétés de sécurité d'un système d'information, cette mise en œuvre a un coût certain : temps de développement, connaissances requises, technicité du développement ... Aussi, il convient de chercher à réduire ce coût non seulement en étudiant les techniques de réutilisation de développements formels, en outillant ces méthodes, mais aussi en concevant des cadres génériques dédiés aux domaines considérés et permettant de factoriser le travail de développement. Une partie du chapitre 1 est consacrée à cette problématique et
<figure><img src="image_4.png" /><figcaption>FIG. 1 – Incidents de sécurité (Source : enquête 2005 du CLUSIF)</figcaption></figure>

le chapitre 2 est dédié à la construction *ex-nihilo* d'un nouveau cadre générique dédié à un domaine particulier, celui du contrôle d'accès, domaine sur lequel repose, en partie, la sécurité des systèmes d'information.

Selon Vinton Cerf, co-fondateur du protocole TCP/IP, entre 100 et 150 millions des 600 millions d'ordinateurs connectés à Internet sont actuellement sous le contrôle direct de pirates<fnref n="1" />. Ces ordinateurs sont utilisés à l'insu de leur propriétaire légitime afin d'effectuer toutes sortes d'actions illégales, comme l'envoi de “spam” ou des attaques contre des serveurs. De fait, la maîtrise de l'information est devenue aujourd'hui un enjeu primordial pour les états, pour les entreprises mais aussi pour les citoyens. En 2005, le CLUSIF (Club de la Sécurité de l'Information Français) fournissait une classification d'incidents de sécurité et une estimation quantifiée des causes de ces incidents. Les résultats de cette étude, présentés dans la figure 1, montrent que 58% des incidents de sécurité sont dûs à des erreurs de conception. Les domaines liés à la sûreté (nucléaire, ferroviaire, aérospatiale, etc) ont mis en place un arsenal de mesures et techniques pour la spécification, la conception et l'implantation des parties logicielles d'un système, permettant de déjouer les menaces causées par l'usure des composants, les perturbations de transmission des signaux, etc. Dans les domaines liés à la sécurité, de tels procédés, destinés à déjouer les menaces relatives aux attaques informatiques, ne sont mis que lentement en place et de manière encore trop parcellaire. Les demandes de tels outils sont d'autant plus pertinentes que l'intégration des communications réseaux dans les grands systèmes informatiques abolit toute notion de barrière physique de protection. Dans le domaine du logiciel, les Critères Communs [22] fournissent une méthodologie permettant d'atteindre des hauts niveaux de sûreté. Les hauts niveaux de sûreté des Critères Communs (EAL – *Evaluation Assurance Level* – 5 à 7) requièrent l'utilisation de méthodes formelles dans les étapes de spécification et de conception du logiciel.

La sécurité d'un système d'information repose sur plusieurs mécanismes aux objectifs différents :

<footnote n="1">¹Article de la BBC du 25/01/07.</footnote>
- Prévenir : Empêcher les attaques (moniteur de référence, mécanismes d'isolation, de confinement, etc).

- Résister : Limiter la portée des attaques (pare-feu, "chroot", cloisonnement, etc).

- Détecter : Surveiller le système pour identifier les attaques (systèmes de détection d'intrusion, analyse de "logs", etc).

- Réparer : Remettre en état le système après les attaques (sauvegarde, récupération d'informations, etc).

Dans ce document nous abordons principalement les aspects liés à la prévention et plus particulièrement au contrôle d'accès. En effet, le contrôle des flots d'information dans les réseaux et dans les systèmes d'information est un élément clé dans la construction de la sécurité d'un système informatique. Ce contrôle nécessite de développer des mécanismes permettant de filtrer les accès afin de ne laisser passer que ceux autorisés, et donc de définir une politique de sécurité, c'est-à-dire la caractérisation des accès permis. Le programme chargé de mettre en application cette politique, le moniteur de référence, est souvent considéré comme l'une des clés de voûte de la sécurité d'un système. Sa conception et son développement doivent être menés de manière à garantir sa fiabilité et sa sûreté. En effet, toute faille au sein de ce programme pourrait entraîner des violations de la politique de sécurité. L'emploi des méthodes formelles dans le développement d'un moniteur de référence permet de garantir que certaines propriétés sont toujours respectées.

Ce document synthétise les activités de recherche que j'ai effectuées dans les domaines évoqués dans cette introduction. Le chapitre 1 présente un ensemble de formalisations effectuées avec les systèmes Coq et Focal, ainsi qu'un ensemble de techniques pour permettre une plus grande réutilisabilité des développements formels obtenus. Le chapitre 2 présente les développements effectués dans le domaine du contrôle d'accès. Il s'agit d'un travail démarré en 2004 en collaboration avec C. Morisset et depuis 2007, avec L. Habib. On peut également lire ce chapitre 2 comme un exemple de formalisation à base de mathématiques classiques et de logique d'un domaine de connaissance donné, formalisation dont on suivra les évolutions, rendues nécessaires pour refléter plus exactement les caractéristiques du domaine étudié, au fur et à mesure de leur explicitation. Il est intéressant de noter comment, un certain niveau de formalisation étant atteint, des questions non formulables jusque là deviennent explicites. Y répondre conduit à revoir la formalisation mise en place pour faire émerger les concepts restés enfouis dans la connaissance des experts du domaine. Du fait de la limitation imposée sur le nombre de pages, plusieurs annexes permettent d'éclairer certaines parties du document : l'annexe A présente rapidement l'atelier Focal, l'annexe B explicite les formalisations réalisées dans le domaine de la programmation logique, l'annexe C décrit sur des exemples concrets les techniques mises en œuvre pour faciliter la réutilisation de développements formels et l'annexe D complète le chapitre 2 par un ensemble de définitions, de propriétés et d'exemples.
# Chapitre 1

## Développements formels

Les travaux présentés dans ce document ont en commun l'utilisation de méthodes formelles. Ces travaux portent sur des objets variés mais partagent un même objectif : obtenir une description formelle de ces objets à un niveau de détail proche de celui d'une implantation afin de mieux les comprendre, d'en garantir les propriétés fondamentales et éventuellement d'en construire une implantation certifiée. Formaliser un algorithme, la sémantique d'un langage, ou encore certains aspects liés à la sécurité d'un système d'information permet d'en donner une description au travers de définitions et de spécifications non ambiguës et explicites. Cette description s'accompagne d'un ensemble de propriétés dont les preuves reposent sur les définitions. Le niveau de détail visé lors de ce travail de formalisation doit permettre de garantir ces propriétés, grâce à la mécanisation des définitions et des raisonnements à l'aide de systèmes d'aide à la preuve.

La première partie de ce chapitre (section 1.1) décrit un ensemble de développements formels réalisés en essayant de dégager les apports obtenus par le travail de formalisation. Certains de ces travaux sont développés en annexe B. Les formalisations que j'ai réalisées portent essentiellement sur la logique (unification, sémantique de la programmation logique, formalismes logiques) durant la période 1997-2003, et depuis 2004, sur le contrôle d'accès. L'ensemble des travaux présentés dans la section 1.1 a permis d'aborder la problématique de la réutilisation de développements formels et de l'ingénierie de la preuve. En effet, si les systèmes d'aide à la preuve connaissent une utilisation croissante, trop souvent encore, écrire une preuve formelle nécessite de spécifier à partir de "presque rien" (i.e. "from scratch") les objets considérés avant de construire les preuves des propriétés que l'on souhaite obtenir.

Formaliser une théorie, c'est décrire dans un langage formel les objets de cette théorie, exprimer, dans ce même langage, les propriétés que ces objets peuvent vérifier et prouver certaines d'entre elles, souvent à l'aide d'un langage de tactiques. Il s'agit donc d'un développement de logiciel et la problématique de la réutilisation de développements formels est naturellement proche de celle de la réutilisation de programmes. On retrouve donc les notions classiques de modularité, de généricité, d'abstraction ... qui sont des critères importants de réutilisabilité. Une approche par réutilisation pose cependant quelques problèmes. En effet, rares sont les formalisations directement réutilisables : on peut distinguer trois classes de contexte de réutilisation :

- La formalisation existante porte sur un "problème isomorphe" et il reste à "transposer"
les propriétés formelles du “domaine existant” (ou d’un sous-ensemble de ce domaine) au domaine considéré.

- La preuve existante est “presque identique” et il suffit de l’adapter.

- Les définitions et les preuves formelles existantes sont génériques (i.e. paramétrées) et il suffit d' “instancier” l'existant pour obtenir directement la formalisation souhaitée (il s'agit là de la situation idéale).

Dans la section 1.2, nous illustrons chacune de ces situations à l'aide d'exemples concrets et esquissons les méthodes mises en œuvre pour réutiliser effectivement des développements formels existants. Une présentation plus détaillée de ces travaux est donnée en annexe C.

# 1.1 Formalisations

Nous présentons dans cette section les formalisations effectuées en indiquant ce que l'activité de formalisation a permis de comprendre et/ou de corriger.

## 1.1.1 Unification et SLD-résolution

Les résultats fondamentaux de la programmation logique sont en général exposés en omettant les détails techniques relatifs aux mécanismes de renommage mis en œuvre lors de l'exécution de programmes logiques. Pourtant, ces mécanismes jouent un rôle important et sont sources d'erreur dans certains énoncés et preuves. Ces détails ne peuvent pas être ignorés si l'on souhaite effectivement implanter un mécanisme d'exécution des programmes logiques. La spécification de la manipulation des identificateurs, et donc de la sémantique opérationnelle d'un langage, doit être suffisamment explicite pour l'implanteur d'un inter-préteur ou d'un compilateur pour ce langage. Afin d'explicitier ces mécanismes, j'ai donc formalisé, dans le système Coq, les propriétés essentielles de la SLD-résolution, mécanisme de base de la programmation logique.

Le langage de programmation logique étudié (correspondant au noyau logique de Pro-log) a été représenté dans le langage du Calcul des Constructions. Deux plongements de nature différente ont été réalisés. Dans un premier temps, un “plongement profond” (deep embedding) a été effectué [59, 61] : il s'agit ici de représenter la syntaxe abstraite d'un langage, le langage “plongé” (langage de la programmation logique), par un type d'un autre langage, le langage “de plongement” (le langage du Calcul des Constructions) puis de définir la sémantique du langage plongé dans le langage de plongement. Cette approche permet d'analyser finement le langage “plongé”. Dans un deuxième temps, un “plongement superficiel” (shallow embedding) a été effectué [62, 64, 63, 65] : il s'agit ici de représenter un programme du langage “plongé” par un programme du “langage de plongement”. Cette approche permet d'analyser les programmes “plongés” mais ne permet pas de prouver dans le langage de plongement les propriétés du langage plongé.

A partir d'une formalisation de l'unification au premier ordre, pour obtenir un plongement profond du langage de programmation logique, j'ai formalisé tout d'abord la sémantique opérationnelle des programmes logiques, définie par la SLD-résolution et basée sur le mécanisme d'unification. Cela m'a conduit à explicitier totalement et *a priori* les conditions de renommage des variables mises en jeu lors d'une SLD-dérivation et cela m'a
permis de détecter certaines erreurs et confusions dans la littérature. Deux lemmes classiques de généralisation et de commutation ont pu être prouvés dans le système Coq. Le premier permet d'établir que si l'exécution d'un programme logique à partir d'une requête R "réussit", alors l'exécution de ce programme à partir d'une requête dont R est une instance "réussit" aussi. Le deuxième permet d'établir que le non-déterminisme dans le choix de l'atome sélectionné à chaque étape de résolution relève d'un non-déterminisme par indifférence. Enfin, la sémantique déclarative des programmes a été décrite dans ce même cadre et les preuves des deux résultats fondamentaux de validité et de complétude de la SLD-résolution ont pu être mécanisées. Ces deux preuves ont été obtenues en suivant l'approche "traditionnelle" introduite par M.H. van Emden et R.A. Kowalski dans [124]. Cette approche utilise les notions d'interprétations de Herbrand et de points fixes d'un opérateur continu associé à tout programme et correspond à celle que l'on peut trouver dans la plupart des ouvrages de base consacrés à la programmation logique. Bien sûr, d'autres approches plus récentes ont été développées pour établir ces résultats, mais notre objectif n'était pas d'écrire *une* preuve formalisée de ces résultats, mais *la* preuve traditionnelle de ces résultats. Les sections B.1 et B.2.1 décrivent plus amplement l'ensemble de ce travail.

Alors que les résultats classiques de la programmation logique concernent la sémantique des calculs finis, certains programmes logiques peuvent donner lieu à des exécutions infinies. Pour de tels programmes, ces résultats ne s'appliquent pas et il n'existe pas une unique "sémantique classique" mais plusieurs approches non équivalentes. Dans la plupart d'entre elles, la dénotation d'un programme logique *P* est obtenue en considérant le plus grand point fixe d'un opérateur associé à *P*. Hélas, lorsque l'univers du discours contient des éléments infinis, l'utilisation d'un plus grand point fixe conduit à définir une sémantique valide mais non complète (i.e., certains éléments apparaissant dans la dénotation d'un programme *P* ne sont pas "constructibles" par une exécution de *P*). Les approches existantes sont exclusivement dédiées à la caractérisation d'objets infinis. L'approche que nous avons développée correspond à une démarche "opposée" : l'univers du discours considéré ne contient pas d'éléments infinis et seules les exécutions ne construisant aucun terme infini sont considérées. Il s'agit là d'une restriction qui permet de définir une sémantique complète en terme de plus grand point fixe d'un opérateur associé au programme considéré.

Comme point de départ pour cette étude des exécutions infinies, les preuves SLD, finies ou infinies, engendrées pas les exécutions d'un programme logique ont été comparées à celles que l'on peut obtenir, par induction ou par co-induction, à partir des clauses d'un programme logique vues comme des règles d'inférence (les dérivations infinies ont été interprétées selon l'isomorphisme de Curry-Howard en identifiant ces dérivations infinies à des λ-termes d'un type co-inductif). Cette lecture sémantique permet de considérer un programme, non plus comme une théorie du premier ordre, mais comme un ensemble de définitions (co-)inductives. Dans le cas fini, la correspondance entre preuves et SLD réfutations est complète. Dans le cas infini, certains objets non calculables (par une SLD dérivation) sont toutefois prouvables (par co-induction), la correspondance est donc incomplète. Un plongement superficiel de la programmation logique dans le Calcul des Constructions permet non seulement d'expliquer ce phénomène d'incomplétude mais aussi de définir une sémantique valide et complète pour une classe d'exécutions infinies. Ce travail est décrit dans la section B.2.2.
### 1.1.2 Modèles de contrôles d'accès

Nous présentons à présent les formalisations réalisées dans le domaine de la sécurité informatique, et plus précisément dans le domaine du contrôle d'accès. Différentes politiques de sécurité peuvent être utilisées pour définir un mécanisme de contrôle d'accès. Toutefois, rien ne sert de mettre en place une politique de sécurité pour gérer un système si les programmes chargés de garantir le bon fonctionnement de cette politique ne sont pas fiables. Cette section rend compte de manière informelle de différentes expériences réalisées depuis 2004 en collaboration avec E.Gureghian, T.Hardin et C.Morisset, synthétisées dans [70], afin d'obtenir des développements formels de politiques de contrôle d'accès. Comme nous le verrons, ces développements nous ont conduit à introduire un "cadre sémantique", présenté dans le chapitre 2, dans lequel il est possible de spécifier par étapes successives, d'implanter et de comparer des politiques de contrôle d'accès.

Les travaux présentés dans cette section ont pour objectif de certifier des programmes en charge de la sécurité dans un système d'information. Plus précisément, il s'agit de garantir qu'un moniteur de référence chargé du contrôle des accès dans un système maintient une politique de contrôle d'accès donnée. Cette propriété est bien sûr cruciale pour la plupart des systèmes d'information. Aux difficultés déjà évoquées dans la section 1.1.1 s'ajoutent avec cet exemple celles liées au passage de l'informel au formel. En effet, bon nombre de politiques sont exprimées de manière informelle dans la littérature. Pour illustrer cela, considérons l'exemple classique de la politique de la Muraille de Chine, introduite par D.F.C. Brewer et M.J. Nash [19], pour résoudre les problèmes de conflit d'intérêt dans le monde des consultants. Chaque objet du système appartient à un ensemble de données d'une compagnie, et chaque compagnie appartient à une unique classe de conflit d'intérêt. Ces classes de conflit correspondent à des milieux professionnels distincts, comme par exemple les banques ou les compagnies pétrolières. Selon cette politique, un consultant peut travailler en même temps pour une banque et une compagnie pétrolière, mais ne peut pas le faire pour deux banques ou deux compagnies pétrolières. Il existe de plus une classe de conflit spéciale qui ne contient qu'une seule compagnie et qui contient les informations "sanitisées", c'est-à-dire celles qui peuvent être lues par tout le monde sans provoquer de conflit d'intérêt. La politique est énoncée comme la combinaison de deux propriétés de sécurité. Ces deux propriétés sont volontairement répétées en anglais, afin de permettre au lecteur de mieux percevoir le niveau de formalisation de la description originale de cette politique. La première est la règle dite de sécurité-simple :

[19] Access is only granted if the object requested : (a) is in the same company dataset as an object already accessed by that subject, i.e. within the Wall, or (b) belongs to an entirely different conflict of interest class.

La deuxième est celle de sécurité-★ :

[19] Write access is only permitted if (a) access is permitted by the simple security rule, and (b) no object can be read which is in a different company dataset to the one for which write access is requested and contains unsanitized information.

Quel est le statut exact d'un objet qualifié de "object can be read" ? Est-ce un objet que le sujet est en train de lire ? ou bien un objet qu'il lira dans l'avenir ? cela signifie-t-il qu'il a les droits pour le faire ? Dans ce dernier cas, cela signifie qu'un sujet voulant écrire
dans un objet doit révoquer tous les droits qu'il a sur des objets appartenant à une autre classe de conflit. D'autre part, dans l'article original [19], il n'est mentionné nulle part que les accès peuvent être relâchés. Cela signifie-t-il qu'il n'est pas possible de le faire, et qu'un accès est éternel ? Dans ce cas, le modèle de la Muraille de Chine est très restrictif, puisqu'une fois qu'un sujet a écrit dans un objet, il ne peut plus avoir d'accès en lecture ou en écriture à un objet d'une classe de conflit différente. Pour formaliser ces deux propriétés de sécurité, il faut faire des choix quant à l'interprétation de ces propriétés. Le danger provient de ces choix qui permettent plusieurs formalisations non équivalentes de cette politique. Enfin, l'étape de formalisation permet de distinguer clairement d'une part les propriétés de sécurité souhaitées et d'autre part le moniteur de référence chargé de les faire respecter. En effet, la présentation informelle de la politique de la Muraille de Chine peut s'apparenter à une description algorithmique de la fonction d'autorisation des accès. Cela peut amener à considérer immédiatement le "comment", donc l'implantation, au lieu de réfléchir d'abord au "quoi", c'est-à-dire à la spécification de la politique de sécurité.

Formalisation du modèle de Bell & LaPadula dans le système Coq

Nous présentons ici brièvement une formalisation du modèle de Bell et LaPadula [80, 12] dans le système Coq à partir de laquelle un programme certifié implantant un moniteur de référence pour cette politique a été extrait. Ce travail est décrit dans [47]. Il a été effectué en collaboration avec T.Hardin et E.Gureghian et a servi de guide à l'élaboration d'un projet industriel dans la société employant E.Gureghian.

**Politique de Bell & LaPadula** La politique de Bell et LaPadula est habituellement décrite par une machine à états [80, 12]. Elle dépend d'un ensemble $\mathcal{S}$ de sujets, d'un ensemble $\mathcal{O}$ d'objets, d'un ensemble $\mathcal{A}$ de modes d'accès et d'un treillis fini $(\mathcal{L}, \preceq, \Upsilon, \lambda)$ de niveaux de sécurité. Un état du système est décrit par un quadruplet $(m, D, f_s, f_o)$ où $m$ est l'ensemble des accès courants effectués dans le système, $D$ est l'ensemble des droits d'accès et $f_s: \mathcal{S} \to \mathcal{L}$ (resp. $f_o: \mathcal{O} \to \mathcal{L}$) est une fonction associant un niveau de sécurité aux sujets (resp. aux objets). Les éléments de $m$ et de $D$ sont des accès représentés par des triplets de la forme $(s, o, a)$ : $(s, o, a) \in m$ signifie qu'un sujet $s$ accède à un objet $o$ selon le mode d'accès $a$ tandis que $(s, o, a) \in D$ signifie qu'un sujet $s$ dispose des droits (discrétionnaires) pour accéder à un objet $o$ selon le mode d'accès $a$. Les trois propriétés de sécurité définies dans la politique de Bell et LaPadula sont les suivantes.

- Propriété DAC (Discretionary Access Control) : La propriété DAC exprime simplement que tout accès courant est conforme aux droits d'accès. Plus formellement, cette propriété s'écrit :

$$m \subseteq D$$

- Propriétés MAC et MAC\* (Mandatory Access Control) :

- La propriété MAC connue sous le nom de “no read-up property” exprime qu’un sujet ne peut accéder en lecture à un objet que si son niveau de sécurité est supérieur à celui de l’objet accédé. Plus formellement, cette propriété s’écrit :

$$(s, o, \text{read}) \in m \Rightarrow f_s(s) \succeq f_o(o) \qquad (1.1)$$

- La propriété MAC\* connue sous le nom de “no write-down property” permet d’éviter qu’un sujet “malicieux” recopie de l’information sensible à un niveau de sécurité
inférieur. Plus formellement, cette propriété s'écrit :

$$((s, o_1, \mathbf{read}) \in m \land (s, o_2, \mathbf{write}) \in m) \Rightarrow f_o(o_1) \preceq f_o(o_2) \quad (1.2)$$

**Certification d'un moniteur de référence** Nous esquissons ici les grandes lignes de la formalisation du modèle de Bell et LaPadula dans le système Coq. Une description détaillée de ce développement est présentée dans [47]. Ce développement est paramétré par $S, O, A$ et un treillis $(\mathcal{L}, \preceq, \gamma, \lambda)$. Ce treillis est en fait obtenu à partir de deux paramètres : un ensemble $\mathcal{K}$ de "domaines" (connu sous le nom de "needs-to-know"), comme par exemple $\{\text{nucléaire}, \text{médical}, \dots\}$, et un ensemble $\mathcal{C}$ de classifications, comme par exemple $\{\text{Top-secret}, \text{secret}, \text{public}, \dots\}$, muni d'une relation d'ordre total. $\mathcal{L}$ est alors défini comme le treillis produit $\mathcal{C} \times T_k$ où $T_k = (\wp(\mathcal{K}), \subseteq, \cup, \cap)$ est le treillis des parties de $\mathcal{K}$.

A partir de la définition de l'ensemble $\Sigma$ des états, les fonctions de transition sont définies comme des fonctions de $\mathcal{R} \times \Sigma$ dans $\mathcal{D} \times \Sigma$ où $\mathcal{R}$ est un ensemble de requêtes et $\mathcal{D} = \{\text{yes}, \text{no}\}$ contient les réponses possibles<fnref n="1" />. Une fonction de transition $\tau$ correspond à la mise en application d'une politique de sécurité. Elle sera qualifiée de fonction "sûre" si et seulement si elle préserve les propriétés de sécurité, c'est-à-dire si et seulement si elle transforme chaque état vérifiant les propriétés DAC, MAC et MAC* en états vérifiant encore ces propriétés.

Le développement réalisé consiste en une implantation dans Coq de la fonction de transition $\tau_{BLP}$ introduite par Bell et LaPadula ainsi que de la preuve mécanisée du célèbre "Basic Security Theorem" [12] affirmant que $\tau_{BLP}$ est "sûre". Le mécanisme d'extraction de Coq a permis, à partir de cette preuve, d'obtenir un programme certifié qui implante $\tau_{BLP}$.

Ce travail de mécanisation de la preuve a non seulement fourni une implantation avec un niveau de confiance élevé mais a aussi permis de reconnaître, parmi les hypothèses sur la fonction de transition, celles qui sont nécessaires au maintien de la politique de sécurité. Cela permet donc d'envisager des variantes de la fonction $\tau_{BLP}$ qui préservent les propriétés de sécurité.

Toutefois, si elle remplit ses objectifs en termes de garantie de correction, une telle approche peut conduire à des développements difficilement réutilisables. En effet, la moindre modification tant sur la spécification de la politique que sur son implantation conduit à modifier une preuve de plus d'un millier de lignes. Il s'agit là d'un exercice particulièrement chronophage. Pour faciliter la réutilisation, il m'est apparu nécessaire d'élaborer un cadre formel caractérisant les éléments communs aux politiques de contrôle d'accès et permettant d'en dériver progressivement la spécification complète de la politique choisie, puis différentes implantations. Il est également préférable d'utiliser un environnement de développement qui facilite l'implantation de ces différents traits. Même si le système Coq dispose à présent de mécanismes permettant de conduire des développements formels de manière modulaire, nous avons choisi d'utiliser l'atelier Focal, mieux adapté car offrant des traits objets<fnref n="2" />. La section qui suit présente une expérience selon cette approche.

<footnote n="1">¹On peut facilement considérer un ensemble fini de réponses.</footnote>

<footnote n="2">²De plus, l'existence de la bibliothèque de calcul formel [112] permet d'envisager aisément l'implantation dans Focal d'un cadre générique pour le contrôle de d'accès, un tel cadre faisant appel à de nombreuses structures algébriques classiques (treillis, algèbres de Boole, ...).</footnote>
<figure><img src="image_5.png" /><figcaption>FIG. 1.1 – Algèbre des modèles de sécurité de McLean</figcaption></figure>

## Implantation de l’algèbre des modèles de sécurité de McLean

Afin de faciliter la réutilisation des développements formels de modèles de contrôle d’accès, nous avons choisi de définir, dans l’environnement de développement Focal [110, 38], l’“algèbre des modèles de sécurité” introduite par McLean [89]. Ce cadre générique pour le contrôle d’accès peut ensuite être instancié afin d’en dériver une implantation de la politique de Bell et LaPadula, qui peut à son tour être utilisée pour gérer les accès à une base de données relationnelle. Nous décrivons ici l’architecture de l’ensemble de ces développements qui sont détaillés dans [93, 67, 68, 14, 15]. Ce travail a été réalisé en collaboration avec C.Morisset.

### Algèbre des modèles de sécurité
Pour factoriser le travail de formalisation et de développement, il nous fallait trouver un cadre abstrait suffisamment générique pour considérer chacune des politiques envisagées comme une instance de ce cadre. A notre connaissance, le seul cadre générique existant était l“algèbre des modèles de sécurité”, introduite par J. McLean en 1988 [89], qui permet la description d’une politique de contrôle d’accès à trois niveaux de spécification différents (figure 1.1) : les frameworks, les modèles et les systèmes.

Le framework décrit l'environnement : il est paramétré par $S$, $O$, $A$ et un treillis $\mathcal{L}$ et spécifie quels sont les ensembles de sujets qui pourront conjointement demander à accéder à un objet ou demander à changer le niveau de sécurité d'un sujet ou d'un objet (sans toutefois spécifier comment sera traitée cette demande). J.Mc Lean introduit donc la notion d'accès conjoints : certaines opérations ne peuvent être autorisées que si elles sont demandées par un certain groupe de sujets<fnref n="3" />. Dans le cas le plus général, les ensembles de sujets qui pourront conjointement soumettre une requête sont des parties non vides quel-

<footnote n="3">³L'exemple le plus classique vient du monde militaire, où pour lancer un missile, il faut que des personnes habilitées appuient sur un bouton en même temps.</footnote>
conques de $\mathcal{S}$ (toute opération est initiée par au moins un sujet) mais il peut exister des contraintes sur ces ensembles. Par exemple, certaines politiques imposent que si un groupe de sujets peut conjointement soumettre une requête, alors tout sous-ensemble de ce groupe peut également soumettre cette requête. Dans le cas le plus courant, sans accès conjoints, les seuls ensembles autorisés à soumettre une requête sont les singletons construits à partir de $\mathcal{S}$. Les différentes possibilités pour les ensembles de sujets permettent de construire une hiérarchie de frameworks permettant de factoriser les spécifications.

La notion de modèle a été introduite par J.McLean afin de pallier aux problèmes posés par des systèmes de contrôle d'accès ne fixant aucune règle régissant le changement de niveau de sécurité d'un sujet ou d'un objet. La notion de modèle est paramétrée par celle de framework. Un modèle spécifie quels sont les ensembles de sujets qui seront effectivement autorisés à modifier les niveaux de sécurité. Comme pour les frameworks, les différentes propriétés vérifiées par ces ensembles de sujets permettent de construire une hiérarchie de modèles. Certaines relations et opérations sur les modèles sont définies et permettent d'implanter l'ensemble des modèles comme une instance de treillis distributif.

Les états décrivent les informations relatives aux différents niveaux de sécurité associés aux sujets et aux objets ainsi que les accès courants. Une fois la notion d'état définie, on spécifie par un prédicat quels sont les états sûrs, c'est-à-dire quelle est la politique de sécurité appliquée. C'est à partir de cette notion d'état et de modèle qu'est définie la notion de système. Celle-ci décrit la fonction de transition et les propriétés qu'elle doit vérifier. Cette fonction de transition entre états décrit les changements d'états produits lors des requêtes d'accès émises par les sujets.

Ces trois notions ont été mécanisées dans l'atelier Focal puis utilisées pour traiter le cas particulier de la politique de Bell et LaPadula.

**Détection de flots d'information non autorisés**

Ici encore, l'étape de formalisation et de mécanisation de la formalisation avec Focal a permis de corriger la spécification initiale. En effet, ce travail nous a conduit à identifier un problème dans la définition de l'algèbre des modèles de sécurité. Dans [89], McLean illustre l'utilisation du cadre qu'il introduit en spécifiant en son sein une version enrichie de la politique de Bell et LaPadula, essentiellement en considérant la notion d'accès conjoints. La propriété de sécurité MAC* définie en (1.2) est alors (re)définie comme suit :

[89] a state is ⋆-secure if for any subjects $S_1, S_2$ and objects $o_1, o_2$, if $(S_1, o_1, \text{read}) \in m$ and $(S_2, o_2, \text{write}) \in m$ and the classification of $o_1$ dominates that of $o_2$, then $S_1 \cap S_2 = \emptyset$

Ici, $m$ est l'ensemble des accès courants, $S_1$ et $S_2$ sont des ensembles de sujets et un accès est un triplet $(S, o, a)$ exprimant que les sujets présents dans l'ensemble $S$ accèdent conjointement à l'objet $o$ selon le mode $a$. La formalisation de cet énoncé permet d'obtenir la spécification suivante (figure 1.2) :

$$((S_1, o_1, \text{read}) \in m \land (S_2, o_2, \text{write}) \in m \land f_o(o_2) \prec f_o(o_1)) \Rightarrow S_1 \cap S_2 = \emptyset$$

Par contraposition, cette spécification est équivalente à :

$$((S_1, o_1, \text{read}) \in m \land (S_2, o_2, \text{write}) \in m \land S_1 \cap S_2 \neq \emptyset) \Rightarrow \neg(f_o(o_2) \prec f_o(o_1)) \quad (1.3)$$
<figure><img src="image_6.png" /><figcaption>FIG. 1.2 – Violation de la propriété MAC*</figcaption></figure>

Or, si on se limite au cas où $S_1$ et $S_2$ sont réduits à des singletons, c'est-à-dire si on ne considère pas les accès conjoints, la propriété (1.2) implique la propriété (1.3), mais la réciproque est en général fausse : (1.3) n'implique (1.2) que si l'ordre sur les niveaux de sécurité est total. En général cet ordre est partiel (puisqu'il définit une structure de treillis) et la propriété MAC* n'est alors pas vérifiée (bien que (1.3) soit satisfaite) comme le montre l'exemple suivant (figure 1.3). En respectant la propriété (1.3), un sujet $s_1$ peut accéder simultanément en lecture à un objet de niveau de sécurité $l_1$ et en écriture à un objet de niveau de sécurité $l_2$ tels que $l_1$ et $l_2$ ne soient pas comparables. Un sujet $s_2$ peut alors lire ce dernier objet de niveau $l_2$ et écrire simultanément dans un objet de niveau $l_3$ tel que $l_3$ et $l_2$ ne soient pas comparables mais tel que $l_3$ soit inférieur à $l_1$. Il y a alors une "fuite d'information vers le bas" puisqu'il devient ainsi possible de recopier les informations d'un objet de niveau $l_1$ dans un objet de niveau $l_3 \le l_1$.

L'activité de formalisation permet de mettre en lumière de tels problèmes. Ils peuvent être découverts en essayant de prouver des "énoncés faux" (par exemple en essayant de prouver l'équivalence entre (1.2) et (1.3) lorsque $S_1$ et $S_2$ sont des singletons), mais ils peuvent parfois aussi être découverts en utilisant des méthodes permettant de tester une propriété, par exemple une propriété assurant qu'il n'existe pas de séquence d'accès permettant de copier de l'information de niveau élevé dans des objets de niveaux inférieurs. Pour ce faire, il est possible d'utiliser, dans certaines conditions, un outil de test intégré à l'atelier Focal développé par M. Carlier et C. Dubois [20]. Citons aussi les travaux de C. Morisset et A. Santana de Oliveira [50, 94, 93, 28] qui décrivent un algorithme permettant de détecter la "fuite d'information" correspondant à l'exemple présenté dans cette section à partir d'une spécification de politique par un système de réécriture. La description de politiques de sécurité *via* un système de réécriture a été étudiée par A. Santana de Oliveira dans [28].

**Instanciation du modèle et application**

En définissant, c'est-à-dire en instanciant, chacune des entités spécifiées dans le cadre générique introduit par J.McLean et implanté avec l'atelier Focal, nous avons défini la politique de Bell et LaPadula et avons fourni
<figure><img src="image_7.png" /><figcaption>FIG. 1.3 – Violation de la politique de sécurité</figcaption></figure>

une implantation de la fonction de transition $\tau_{BLP}$ évoquée dans la section 1.1.2. Notons que, cette implantation reste encore relativement générique. Par exemple, elle ne spécifie ni les sujets, ni les objets. En effet, un programme qui implante une certaine politique de contrôle d'accès est *a priori* indépendant du système sur lequel il doit s'appliquer (bases de données, systèmes de gestion de fichiers, ...). Il possède des paramètres destinés à prendre en compte l'environnement concret dans lequel il va s'exécuter. Nous allons maintenant illustrer succintement l'intégration de tels programmes dans un système "concret", une base de donnée relationnelle. Il s'agit ici d'une mise à l'épreuve du terrain de la méthode toute entière. Ce travail a été effectué en collaboration avec C.Morisset (doctorant de 2004 à 2007) et J.Blond (doctorant).

La base de données (MySQL) contient à la fois les données des utilisateurs, et les données relatives à la sécurité (droits d'accès, accès courants, niveaux de classification, "needs-to-know"). Les paramètres du système de Bell et LaPadula obtenu dans le paragraphe précédent sont instanciés par des objets stockés dans la partie "sécurité" de la base de données et les états de ce système sont construits à partir de ces données. Deux tables particulières concernant les sujets et les objets sont présentes dans la zone dédiée aux données relatives à la sécurité de la base de données. La table **sujets** contient pour chaque sujet son identifiant unique, son login, son mot de passe, ainsi que son niveau de sécurité. De même, la table **objets** contient pour chaque objet son identifiant unique, le nom de la table à laquelle il correspond ainsi que son niveau de sécurité. Ainsi, les objets du système d'information sont les tables de la base de données. Une granularité plus fine pour la notion d'objet pourrait être envisagée mais soulèverait des problèmes connus dans le domaine des bases de données pour lesquels des solutions existent mais sortent du cadre de notre
<figure><img src="image_8.png" /><figcaption>FIG. 1.4 – Contrôle d’accès pour un SGBD</figcaption></figure>

prototype<fnref n="4" />.

L'architecture de l'implantation se décompose en trois parties : la politique de sécurité, le gestionnaire de base de données et le moniteur de référence. La partie concernant la politique de sécurité est entièrement définie en Focal et repose sur le modèle de Bell et LaPadula. L'accès au gestionnaire de base de données s'effectue grâce à une interface définie en Focal proposant des fonctions de connexion/déconnexion à la base de données, ainsi que des fonctions permettant l'exécution d'une requête et la récupération du résultat. Ces fonctions reposent sur la librairie ocaml-mysql [1], et sont donc spécifiques au gestionnaire de base de données MySQL. La figure 1.4 illustre le traitement des requêtes effectué par l'application obtenue. Etant donnée une requête SQL soumise par un sujet (authentifié), le programme d'analyse de requêtes SQL que nous avons développé fait appel au système de Bell et LaPadula et, selon la réponse obtenue, traite ou refuse l'exécution de la requête soumise. Pour cela, nous avons défini pour chaque requête SQL, un ensemble de requêtes pour le système de Bell et LaPadula, donnant en quelque sorte une sémantique en termes d'accès aux requêtes SQL. On remarquera que les requêtes SQL soumises par l'utilisateur utilisent la syntaxe standard de SQL, rendant ainsi transparente pour l'utilisateur la mise en œuvre de notre application, qui peut être vue comme un filtre entre l'utilisateur et le système de gestion de la base de données. Ce développement est décrit en détail dans [93, 14, 15].

**Nécessité de définir un cadre plus générique** S'il permet de caractériser certains aspects communs à différentes politiques de contrôle d'accès, le cadre introduit par McLean n'est pas encore suffisamment riche. Il est certes est bien adapté à la définition de politiques basées sur un ensemble de niveaux de sécurité associés à certaines entités du système mais ne permet pas de définir des politiques comme la Muraille de Chine (dans le contexte de la Muraille de Chine nous ne disposons pas d'un treillis de niveaux de sécurité mais d'un

<footnote n="4">⁴Par exemple, considérer les tuples d'une base de données comme des objets conduit à un phénomène de polyinstanciation [116] lorsque deux tuples ont la même clé primaire, mais des informations de niveaux de sécurité différents ([13] propose des solutions à ce problème).</footnote>
ensemble de classes de conflits) ou encore des politiques à base de rôles (dans le contexte d'une politique à base de rôles, nous ne disposons pas d'un treillis de niveaux de sécurité mais d'un ensemble de rôles muni d'un ordre partiel). Le cadre de McLean se révèle donc à la fois trop contraignant et trop peu expressif (en termes de propriétés de comparaison de modèles et de simulation d'implantations permettant une plus grande réutilisabilité). Nous avons alors été amenés à concevoir (en 2005) un cadre sémantique pour le contrôle d'accès permettant de répondre à nos objectifs. Il ne s'agit pas de la définition d'un langage mais plutôt d'une spécification de style mathématique de ce qui constitue une politique de contrôle d'accès. Ce cadre et son utilisation sont présentés dans le chapitre 2. Il a été implanté avec l'atelier Focal et instancié pour obtenir une implantation des principales politiques que l'on peut rencontrer dans la littérature : [18] décrit une implantation de politique discrétionnaire à base de matrice de droits d'accès [79, 51] développée en 2007, [6] décrit les implantations obtenues en 2008 d'une politique à la Unix intégrant la notion de groupes d'utilisateurs, d'une politique à base de "tickets" [83], et d'une politique discrétionnaire intégrant un mécanisme de délégation, [93] décrit une implantation de la politique de Bell et LaPadula [80, 12] développée en 2006 et [48] décrit une implantation obtenue en 2007 d'une politique à base de rôles (RBAC96) [42, 117]. L'ensemble de ces développements a été effectué lors de stages que j'ai encadrés.

## 1.2 Réutilisation de développements formels

Dans cette section nous commentons les travaux portant sur la réutilisation de développements formels. Nous avons expérimenté deux approches distinctes. La première relève de l'ingénierie de la preuve et consiste essentiellement à décrire comment exploiter une preuve existante pour obtenir une preuve. Elle est présentée dans la section 1.2.1. La deuxième approche repose sur le constat qu'un développement formel est plus facilement réutilisable s'il a été conduit de manière modulaire et générique. Elle est présentée dans la section 1.2.2.

### 1.2.1 Ingénierie de la preuve

Tandis que les spécifications formelles des définitions des objets et des propriétés sont généralement assez facilement réutilisables, la réutilisation des preuves est par contre plus délicate. Nous allons voir au travers de trois exemples les problèmes posés par la réutilisation de preuves formelles et les solutions possibles. La réutilisation est ici abordée dans divers contextes, la preuve à réutiliser pouvant avoir été obtenue au sein d'un outil de formalisation différent de celui utilisé pour la preuve souhaitée. La manipulation (parcours, recherche, modification, transformation ...) d'une preuve est difficile et peu outillée (citons toutefois [40, 105, 16]) si l'on reste au niveau du langage de tactiques. L'accès à la structure d'une preuve, au niveau de l'utilisateur, est rarement aisé et nécessite une connaissance des représentations internes des preuves, donc du code source de l'outil de développement formel utilisé. On peut envisager de travailler directement sur le terme de preuve mais, au moins en théorie de types, la complexité et la taille d'une preuve ne permettent pas d'envisager l'écriture de la preuve elle-même qui ne figure donc pas dans le code source du développement (les preuves y sont exprimées *via* une suite de tactiques).
## Définition d'isomorphismes

Souvent, il existe plusieurs manières de représenter un même objet. Le choix de la représentation est en général dicté par le traitement que l'on souhaite effectuer sur ces objets. Lorsque le développement formel existant porte sur un problème isomorphe au problème à traiter, c'est à dire lorsque le problème à traiter porte sur des objets obtenus par changement de représentation, la réutilisation consiste à définir des fonctions permettant de passer d'une représentation à une autre et à montrer la préservation des propriétés considérées. Les techniques de changement de représentation ont déjà été étudiées dans [92, 11, 86]. J'ai également considéré ce problème en reprenant les travaux de J.Rouyer [115] sur les quasi-termes, structure de données plus générale que celle des termes. J'ai construit une traduction des quasi-termes vers les termes (fonction partielle) et j'ai ainsi transposé les propriétés de l'unification des quasi-termes à l'unification des termes. L'annexe B.1 détaille le traitement de l'unification au premier ordre et le passage des quasi-termes aux termes fait l'objet de l'annexe C.1.1 et de [60].

Nous avons donc utilisé le mécanisme de réutilisation d'une preuve formelle suivant : considérer la preuve existante comme une boîte noire et construire des "passerelles" – des ponts formels – entre le domaine sur lequel porte la preuve existante et le domaine sur lequel porte la preuve cherchée. Il reste ensuite à prouver que les propriétés souhaitées sont bien conservées par les transformations définies.

## Outil externe de transformation de preuve

Nous présentons maintenant une approche différente pour laquelle la preuve à réutiliser n'est pas considérée comme une boîte noire mais comme un objet sur lequel des transformations vont être effectuées.

Le problème est de réutiliser une preuve établie dans le système Coq pour obtenir une preuve dans l'atelier Focal. Bien sûr, la proximité entre Coq et Focal facilite cette réutilisation. L'environnement Focal, présenté en annexe A, propose un langage d'expression de propriétés qui peuvent être prouvées soit directement à l'aide de Coq, soit à l'aide de l'outil Zenon. Dans les deux cas, un terme de preuve Coq s'appuyant sur la structure particulière des objets spécifiés dans l'environnement Focal est construit par le compilateur. Nous avons construit un outil permettant de transformer une preuve établie avec Coq en une preuve réutilisable dans l'environnement Focal. Cet outil permet d'une part de généraliser une preuve en la paramétrant par une relation d'équivalence et un ensemble de propriétés que doit vérifier cette relation (il s'agit essentiellement de propriétés de congruence) et d'autre part de la réutiliser dans Focal. Cette approche a été appliquée pour réutiliser dans l'environnement Focal des preuves établies sur les groupes avec le système Coq. Elle est présentée plus complètement ainsi que l'exemple dans l'annexe C.1.2 et dans [37]. Ce travail a été réalisé en collaboration avec C.Dubois et J.Grandguillot.

## Preuves dans une architecture hiérarchique

Comme nous l'avons déjà mentionné, la problématique de la réutilisation de preuves formelles est proche de celle de la réutilisation de programmes. Toutefois, une difficulté méthodologique supplémentaire apparaît lorsque les preuves sont développées dans une
architecture hiérarchique, comme c'est le cas avec l'atelier Focal dont le langage sous-
jacent est muni de traits objets. Les preuves peuvent alors être faites à différents niveaux
dans la hiérarchie, ce qui introduit de la souplesse dans les développements. Mais se pose
alors la question de la place des preuves dans l'architecture du développement. Doit-on
faire les preuves "le plus tôt" possible (c'est à dire dès que l'on dispose des spécifications et
des définitions nécessaires), comme c'est l'usage en mathématiques ? Doit-on au contraire
faire les preuves "le plus tard" possible (c'est à dire aux feuilles du graphe d'héritage) ? Dans
le premier cas, le mécanisme de redéfinition risque d'invalider les preuves des propriétés
qui reposent sur la définition de l'objet redéfini, tandis que dans le deuxième cas, les
preuves risquent d'être dupliquées. Il n'y a donc pas de réponses définitives à ces questions.
Nous avons dégagé des critères permettant de répondre à ces questions et esquissé une
méthodologie de développement de preuve dans un contexte hiérarchique. Pour chaque
opération, il s'agit principalement de procéder en trois temps : déclarer, spécifier, puis
implanter. Ce travail est décrit dans [109]. Il est de plus rappelé dans l'annexe C.1.3. Il a
été réalisé en collaboration avec V. Prevosto.

1.2.2 Définition de cadres génériques

La situation idéale pour la réutilisation de développements formels correspond au cas
où le développement à réutiliser a été obtenu par instanciation d'un cadre générique. Dans
ce cas, il suffit d'instancier ce cadre de manière différente afin d'obtenir le développement
souhaité. Ainsi, on devrait s'astreindre, au cours de tout travail de formalisation, à la re-
cherche systématique des abstractions possibles afin de déterminer si un cadre générique
utile peut être dégagé (dans le même esprit que le typage de fonctions permet parfois de re-
connaître le caractère polymorphe de certaines fonctions). Il s'agit ici de décrire comment la
définition d'un cadre abstrait générique permet d'obtenir plusieurs développements, dédiés
à des cahiers des charges différents, qui peuvent être obtenus par instanciation du cadre
générique. Bien sûr, la réutilisation d'un ensemble de spécifications formelles génériques
nécessite de respecter le cadre défini par ces spécifications. Ce cadre peut parfois paraître
trop riche ou trop général (et, dans ce cas on préfere le qualifier de "trop compliqué") pour
l'objet à formaliser. Toutefois, conduire un développement au sein d'un cadre générique
bien conçu permet d'une part de factoriser le travail de développement et de le rendre
réutilisable, et d'autre part, de rendre possible la comparaison des notions formaliséss dans
ce cadre.

Spécification de formalismes logiques

L'informatique consomme aujourd'hui beaucoup de formalismes logiques différents.
Tous ces formalismes partagent en fait des notions exprimables de manière générique. Le
cadre unifié que nous avons adopté et implanté dans le système Coq est une variante de la
notion de logiques générales introduite par J. Meseguer [91, 44]. Chacune des logiques est
vue comme une instance de logique générale, ses propriétés s'exprimant alors dans ce cadre.
L'implantation réalisée avec Coq décrit les notions de syntaxe (formules, morphismes), de
sémantique (institutions) et de preuve (déduction). La notion de système formel y est aussi
décrite afin de faciliter la définition des aspects "preuve" d'une logique. Le développement
obtenu a été utilisé pour implanter la logique des propositions et la logique équationnelle.
Ce travail est décrit dans l'annexe C.2 et dans [66]. Il a été réalisé en collaboration avec C.Dubois.

## Spécification de modèles de contrôle d'accès

Dans la section 1.1.2, nous avons présenté la formalisation d'un cadre générique permettant la définition de modèles de contrôle d'accès. Ce cadre, introduit par J.McLean [89], permet de considérer les politiques basées sur un ensemble de niveaux de sécurité partiellement ordonné. Il est donc particulièrement bien adapté pour décrire des (variantes de) modèles à la Bell et LaPadula. Toutefois, il s'est révélé trop contraignant puisqu'il ne permet pas de prendre en compte des politiques exprimées à partir de paramètres de sécurité quelconques (comme c'est le cas avec les modèles à base de rôles et le modèle de la Muraille de Chine). De plus, comme nous l'avons dit, conduire une formalisation au sein d'un cadre générique permet de comparer les objets formalisés. Dans le contexte du contrôle d'accès, cette possibilité peut fournir des critères de choix entre plusieurs politiques de sécurité pour une application donnée. Enfin, comparer des modèles peut conduire à des schémas de traduction d'un modèle vers un autre et fonder ainsi des techniques de réutilisation.

Après l'étude de l'algèbre des modèles de sécurité de J.McLean, nous avons entrepris, en 2006, la définition d'un cadre générique permettant la spécification, l'implantation et la comparaison de modèles de contrôle d'accès. Ce cadre fournit une caractérisation des éléments communs aux politiques de contrôle d'accès et permet d'en dériver différentes implantations. Il fournit plusieurs niveaux de spécification. Nous donnons ici rapidement les grandes articulations de ce cadre, qui sera présenté en détail dans le chapitre 2. Tout d'abord, ce cadre permet de décrire comment est conçu le système d'information considéré, c'est à dire quels sont les paramètres de sécurité mis en jeu et quelles sont les informations qui décrivent l'état du système. La politique de contrôle d'accès peut alors être spécifiée en caractérisant le sous-ensemble des états du système qui sont considérés comme sûrs, c'est à dire qui respectent la politique de sécurité. Ensuite, les requêtes permettant de modifier l'état du système peuvent être spécifiées non seulement par la syntaxe mais aussi par la sémantique du langage de requêtes (quelles sont les modifications attendues sur les états lors de l'exécution d'une requête). Ces deux notions (politique et langage de requêtes) permettent d'introduire la notion de modèle de contrôle d'accès. Ensuite, le cadre défini sert à décrire les implantations possibles d'un modèle par la donnée d'un ensemble d'états initiaux et d'une fonction de transition entre états. Bien sûr, la fonction de transition considérée doit satisfaire des propriétés de correction vis à vis de la politique considérée et vis à vis de la sémantique des requêtes. Puisqu'il existe plusieurs implantations possibles, plus ou moins restrictives, d'un même modèle, une relation de préordre sur les implantations peut être introduite. Enfin, le cadre sémantique proposé fournit également une relation de comparaison entre modèles de contrôle d'accès qui repose sur la notion de simulation d'implantations. La conception de ce cadre ne correspond pas à la définition d'un langage mais plutôt à une spécification abstraite de ce qui constitue une politique de contrôle d'accès. Ce cadre, décrit en détail dans le chapitre 2, a été utilisé avec succès pour spécifier, implanter et comparer les principaux modèles existant dans la littérature.
# Chapitre 2

## Contrôler le contrôle d'accès

La confiance dans un produit passe généralement par un certain nombre d'avis de personnes reconnues comme experts. Ces experts se basent sur des normes pour certifier que le produit en question est conforme aux exigences issues de la demande de confiance. Dans le domaine du logiciel, les Critères Communs [22] (recueil de normes définies par des agences gouvernementales) fournissent une méthodologie permettant d'atteindre des hauts niveaux de sûreté. Ils définissent à la fois un cadre de travail pour la conception et la réalisation de logiciels et une référence pour les utilisateurs de ces logiciels. Les hauts niveaux de sûreté des Critères Communs (EAL – *Evaluation Assurance Level* – 5 à 7) requièrent l'utilisation de méthodes formelles dans les étapes de spécification et de conception du logiciel implantant les fonctions de sécurité afin de justifier la confiance accordée à ces fonctions.

Dans ce chapitre, nous utilisons une démarche formelle pour étudier certaines des propriétés classiques de sécurité des systèmes d'information. Selon les Critères Communs, un système est vu comme une installation donnée de technologies de l'information, avec un objectif et un environnement opérationnel particuliers et une politique de sécurité est un ensemble de règles qui précisent comment gérer, protéger ou distribuer les informations ou ressources du système. Nous nous intéressons ici plus particulièrement aux politiques de contrôle d'accès dont l'objectif est de régir et gérer les accès effectués selon certains modes (lecture, écriture, etc.) par des sujets, les entités actives (processus, programmes, utilisateurs, etc.) sur des objets, les entités passives (données, fichiers, programmes, etc). Mettre en place un mécanisme de contrôle d'accès consiste dans un premier temps à définir la politique de contrôle d'accès à proprement parler, c'est-à-dire spécifier les accès autorisés et ceux interdits. Dans un deuxième temps, il faut définir un moniteur de référence, c'est-à-dire un programme chargé de mettre en œuvre la politique de contrôle d'accès au sein du système. Toujours selon les Critères Communs, un moniteur de référence doit posséder les trois caractéristiques suivantes :

- des sujets non sûrs ne peuvent pas interférer avec son fonctionnement, i.e. il est à l'épreuve d'une intrusion physique,

- des sujets non sûrs ne peuvent pas court-circuiter les contrôles qu'il effectue, i.e. il est systématiquement appelé,

- il est suffisamment simple pour être analysé et pour comprendre son comportement, i.e. sa conception est simple.
Ces trois caractéristiques, introduites dans [5], sont connues sous l'acronyme NEAT, pour "Non-bypassable" (il n'est pas possible d'éviter les fonctions de sécurité), "Evaluable" (les fonctions de sécurité sont suffisamment simples pour être mathématiquement vérifiées et évaluées), "Always Invoked" (les fonctions de sécurité sont systématiquement appelées) et "Tamperproof" (les fonctions de sécurité ne peuvent pas être altérées). Cet acronyme est défini dans le cadre de MILS<fnref n="1" /> (Multiple Independent Levels of Security), une approche de développement de systèmes sécurisés. L'utilisation de méthodes formelles pour la conception d'un moniteur de référence facilite son évaluation et sa vérification, puisque la correction du programme vis-à-vis de sa spécification peut être énoncée et prouvée de manière formelle.

De nombreux modèles de contrôle d'accès existent dans la littérature, comme le modèle de Bell de LaPadula [12], le modèle HRU [51], le modèle de la Muraille de Chine [19], celui à base de rôles [42], sans oublier un ensemble d'extensions de ce dernier, comme le modèle à base d'organisations [72], à base de coalition [24], à base d'équipes [121], etc. Chacun de ces modèles a été conçu pour répondre à un besoin de sécurité précis dans un contexte précis. Néanmoins, certains de ces modèles ne sont pas exprimés de manière formelle, ce qui peut conduire à une mauvaise compréhension, une mauvaise utilisation, voire à une mauvaise implantation de ces modèles. De plus, ces différents modèles ne sont pas tous exprimés dans un même formalisme, et il est ainsi difficile de comparer deux modèles entre eux. Dans ce chapitre, nous présentons donc un cadre formel uniforme permettant la spécification, l'implantation, la comparaison et l'analyse de flots d'information de ces différents modèles de contrôle d'accès.

La suite de ce chapitre est organisée comme suit :

- La section 2.1 présente le cadre sémantique permettant de spécifier et d'implanter les modèles de contrôle d'accès. Ce travail a été réalisé en collaboration avec C. Morisset.

- Dans la section 2.2, nous introduisons des critères à partir desquels nous pouvons définir des relations de comparaison entre implantations d'un modèle mais aussi entre modèles. Ce travail a été réalisé en collaboration avec C. Morisset et L. Habib.

- Dans la section 2.3, nous montrons comment il est possible d'analyser les flots d'information engendrés par les exécutions d'un moniteur de référence. Ce travail a été réalisé en collaboration avec V. Viet Triem Tong et L. Mé.

Ce travail étend les résultats décrits dans [69] et rend compte, en partie, des travaux présentés dans [70, 93, 48, 49, 71]. Les résultats présentés dans ce chapitre sont détaillés et illustrés dans la section D figurant en annexe.

## 2.1 Un cadre sémantique pour la définition de modèles de contrôle d'accès

Nous introduisons ici un cadre permettant non seulement de spécifier et d'implanter des modèles de contrôle d'accès mais aussi de les comparer et d'analyser les flots d'information qu'ils autorisent. Il s'agit d'identifier les "ingrédients" communs aux modèles de contrôle d'accès, d'exprimer les propriétés génériques qu'ils vérifient et de comprendre le rôle de ces

<footnote n="1">¹http://www.ois.com/MILS/</footnote>
"ingrédients" dans une implantation. Ce cadre fournit une spécification abstraite de ce qui constitue un modèle. Il s'agit donc d'un cadre sémantique pour le contrôle d'accès.

### 2.1.1 Politiques de contrôle d'accès

Une politique de contrôle d'accès permet de caractériser les états d'un système et de spécifier ce qu'est un état sûr en fonction d'informations de sécurité associées aux entités du système.

**Entités** Les entités du système peuvent être réparties dans deux ensembles : l'ensemble *S* des sujets, également appelés *entités actives*, qui correspondent aux entités qui effectuent les actions dans le système, et l'ensemble *O* des objets, également appelés *entités passives*, qui subissent les actions. Les sujets et les objets sont généralement considérés comme des entités atomiques. Ces deux ensembles ne sont pas nécessairement disjoints : par exemple, un processus peut à la fois être un sujet et ainsi effectuer des opérations, et un objet, dans le cas où un autre processus tente de l'arrêter.

**Accès** Nous désignons par $\mathcal{A}$ l'ensemble des modes d'accès qui caractérisent les différents types d'accès effectués par les sujets sur les objets. Cet ensemble contient généralement *read*, *write*, *append*, etc. Une approche classique consiste à représenter un accès par un triplet $(s, o, a)$, signifiant que le sujet *s* accède à l'objet *o* selon le mode d'accès *a*. Néanmoins, d'autres approches existent (on peut par exemple regrouper les modes d'accès, ou encore considérer les accès conjoints de sujets sur des objets). Afin de pouvoir prendre en compte ces différentes situations, nous nous limitons à dénoter par $\mathcal{A}$ l'ensemble de tous les accès, sans introduire une véritable définition qui serait trop précise à ce stade.

**Politiques de contrôle d'accès** Les systèmes de contrôle d'accès sont ici modélisés sous la forme de machines à états. Un état représente le système à un instant donné et contient au moins une description de l'ensemble des *accès courants*, c'est-à-dire de tous les accès qui ont été acceptés et qui n'ont pas encore été relâchés. Ces accès sont donc supposés être effectués simultanément dans le système. L'ensemble des états est noté $\Sigma$ et l'ensemble des accès courants d'un état $\sigma$ est noté $\Lambda(\sigma)$ ($\Lambda$ est donc une fonction de $\Sigma$ dans $\wp(\mathcal{A}))$. Une politique de contrôle d'accès permet de spécifier un sous-ensemble de $\Sigma$, contenant les états sûrs, c'est-à-dire les états qui vérifient la politique. Afin de déterminer si un état est sûr, les entités du système sont associées à des informations de sécurité :

- le paramètre de sécurité, noté $\rho$, décrit les informations de sécurité *statiques* de la politique, c'est-à-dire les informations de sécurité qui ne changeront pas durant la vie du système,

- les fonctions de sécurité décrivent les informations de sécurité *dynamiques* de la politique, c'est-à-dire les informations de sécurité susceptibles d'évoluer durant la vie du système (étant donné un état $\sigma$, on note $\Upsilon(\sigma)$ les fonctions de sécurité associées à l'état $\sigma$).

A partir des informations *dynamiques* décrites par un état (ensemble des accès courants et fonctions de sécurité) et des informations *statiques* du système (paramètre de sécurité), les états sûrs sont caractérisés par un prédicat $\Omega$ sur les états. On note $\Sigma|_{\Omega}$ l'ensemble
$\{\sigma \in \Sigma | \Omega(\sigma)\}$ des états sûrs. Toutes ces notions nous permettent de définir une politique de contrôle d'accès comme suit.

**Définition 2.1** Une politique de contrôle d'accès $\mathbb{P}[\rho]$, basée sur un paramètre de sécurité $\rho$, est définie par un quintuplet $\mathbb{P}[\rho] = (S, O, A, \Sigma, \Omega)$.

A ce niveau de spécification, il est possible de caractériser certaines propriétés que peuvent vérifier les politiques de contrôle d'accès. Dans la suite nous utiliserons les deux propriétés suivantes :

- Une politique est dite *compacte* si lorsque l'on supprime des accès de l'ensemble des accès courants d'un état sûr, l'état reste sûr :

$$ \forall \sigma_1 \in \Sigma \quad \Omega(\sigma_1) \Rightarrow (\forall \sigma_2 \in \Sigma (\Lambda(\sigma_2) \subseteq \Lambda(\sigma_1) \wedge \Upsilon(\sigma_1) = \Upsilon(\sigma_2)) \Rightarrow \Omega(\sigma_2)) $$

La plupart des politiques classiques (HRU, Bell et LaPadula, Muraille de Chine, RBAC, ...) sont compactes. Toutefois, il peut être utile de définir des politiques non compactes dans certains contextes. Considérons par exemple une politique de contrôle des accès aux ressources d'un système qui stipule qu'un utilisateur est autorisé à utiliser des ressources d'une équipe à laquelle il n'appartient pas, mais seulement dans le cas où toutes les ressources de son équipe sont déjà accédées. Une telle politique n'est pas compacte puisque lorsqu'un utilisateur accède à une ressource d'une équipe à laquelle il n'appartient pas, retirer un accès sur une ressource de son équipe conduit à un état non sûr.

- Une politique est dite *libre* si lorsqu'un accès est autorisé pour un état sûr du système, il est autorisé pour tous les états sûrs<fnref n="2" /> :

$$ \begin{gathered} \forall \sigma \in \Sigma \quad \forall s \in S \quad \forall o \in O \quad \forall a \in A \\ ((\exists \sigma' \in \Sigma (\Omega(\sigma') \wedge (s, o, a) \in \Lambda(\sigma')) \wedge \Omega(\sigma)) \Rightarrow \Omega(\sigma \oplus (s, o, a)) \end{gathered} $$

Par exemple, HRU définit une politique libre puisque le prédicat caractérisant les états sûrs est défini en examinant chacun des accès courants indépendamment des autres accès en cours. En revanche, la politique de Bell et LaPadula n'est pas libre puisqu'il est possible qu'un sujet soit autorisé à écrire dans un objet lorsque ses accès en lecture vérifient certaines conditions et ne soit plus autorisé à écrire dans cet objet lorsque ses accès en lecture ne vérifient plus ces conditions.

Enfin, étant donné un état $\sigma$, nous introduisons l'ensemble $W(\sigma)$ des ensembles d'accès qui peuvent être ajoutés à l'ensemble des accès courants de l'état $\sigma$, sans changer les fonctions de sécurité, de manière à ce que l'état ainsi obtenu reste sûr :

$$ W(\sigma) = \left\{ \begin{array}{ll} A \in \wp(A) & | \forall \sigma' \in \Sigma \\ (\Upsilon(\sigma') = \Upsilon(\sigma) \wedge \Lambda(\sigma') = \Lambda(\sigma) \cup A) \Rightarrow \Omega(\sigma') & \end{array} \right\} $$

Les ensembles d'accès présents dans $W(\sigma)$ sont appelés les accès potentiels de $\sigma$. Cette définition introduit une "sémantique" sur les états et nous permettra par la suite de définir

<footnote n="2">²$\sigma \oplus (s, o, a)$ (resp. $\sigma \ominus (s, o, a)$) dénote un état tel que :</footnote>

<footnote>$\Lambda(\sigma \oplus (s, o, a)) = \Lambda(\sigma) \cup \{(s, o, a)\}$ et $\Upsilon(\sigma \oplus (s, o, a)) = \Upsilon(\sigma)$ (resp. $\Lambda(\sigma \oplus (s, o, a)) = \Lambda(\sigma) \setminus \{(s, o, a)\}$ et $\Upsilon(\sigma \oplus (s, o, a)) = \Upsilon(\sigma)$)</footnote>
une relation d'équivalence entre les états de systèmes basés sur des politiques différentes. Nous introduisons également la fonction $W_0 : \Sigma \to \wp(\wp(\mathbb{A}))$, qui étant donné un état, retourne tous les ensembles d'accès "compatibles" avec les fonctions de sécurité de cet état. Etant donné un état $\sigma$, $W_0(\sigma) = W(\sigma')$ avec $\Lambda(\sigma') = \emptyset$ et $\Upsilon(\sigma') = \Upsilon(\sigma)$. Ces définitions permettent d'établir plusieurs propriétés "techniques" utiles lors de la comparaison de politiques de contrôle d'accès. On peut montrer par exemple que si un état $\sigma$ est tel que $W(\sigma) = \emptyset$, alors il n'est pas sûr (i.e. $\Omega(\sigma)$ est faux). La réciproque n'est cependant pas vraie dans le cas général mais l'est pour les politiques compactes.

Plusieurs exemples de politiques classiques de contrôle d'accès sont formalisés en an-
nexe D.1.1.

2.1.2 Modèles de contrôle d'accès

Nous introduisons à présent la notion de modèle de contrôle d'accès, qui permet de
spécifier comment passer d'un état du système à un autre. Pour cela, nous introduisons
tout d'abord la notion de langage de requêtes.

Requêtes

Une requête est soumise par un sujet afin de faire évoluer le système, soit en ajoutant
ou en enlevant un accès, soit en changeant les informations de sécurité dynamiques du
système. Dans ce dernier cas, on parle de requêtes administratives. La plupart des modèles
de contrôle d'accès considèrent au moins les droits d'accès read (lecture) et write (écriture).
On peut généralement considérer les requêtes suivantes :

$$
\mathcal{R}^{\text{acc}} = \{ \langle +, s, o, a \rangle, \langle -, s, o, a \rangle \} \tag{2.1}
$$

où $\langle +, s, o, a \rangle$ (resp. $\langle -, s, o, a \rangle$) correspond à la demande du sujet $s$ d'accéder (resp. de relâcher l'accès) à l'objet $o$ selon le mode d'accès $a$. La notion de relâchement d'accès n'est pas nécessairement présente dans tous les modèles de contrôle d'accès. En effet, elle sous-entend la notion (implicite) de persistance des accès, c'est-à-dire qu'une fois qu'ils sont effectués, ces accès restent en mémoire.

Etant donné un ensemble de requêtes $\mathcal{R}$, il est nécessaire d'introduire une sémantique pour le langage de requêtes afin de pouvoir caractériser les modifications sur les états engendrées par l'application de ces requêtes lors d'une transition effectuée par le moniteur de référence qui implante la politique. Nous introduisons ici deux procédés différents pour définir cette sémantique. Ils seront utilisés pour comparer des modèles de contrôle d'accès selon deux techniques différentes.

Le procédé le plus classique pour définir une sémantique du langage des requêtes consiste à introduire une “sémantique de transitions” via une relation $\llbracket \mathcal{R} \rrbracket_{\Sigma}^{+} \subseteq \Sigma \times \mathcal{R} \times \Sigma$. Avec une telle approche, $(\sigma_1, R, \sigma_2) \in \llbracket \mathcal{R} \rrbracket_{\Sigma}^{+}$ permet de spécifier les propriétés d'un état $\sigma_2$ lorsqu'il a été obtenu par application d'une requête $R$ sur un état $\sigma_1$. Par exemple, si l'on considère l'ensemble $\mathcal{R}^{acc}$ introduit plus haut, la relation $\llbracket \mathcal{R}^{acc} \rrbracket_{\Sigma}^{+}$ peut être définie comme suit :

$$
(\sigma_1, \langle +, s, o, a \rangle, \sigma_2) \in \llbracket \mathcal{R}^{acc} \rrbracket_{\Sigma}^{+} \Leftrightarrow (\Lambda(\sigma_2) = \{(s, o, a)\} \cup \Lambda(\sigma_1) \wedge \Upsilon(\sigma_1) = \Upsilon(\sigma_2))
$$

$$
(\sigma_1, \langle -, s, o, a \rangle, \sigma_2) \in \llbracket \mathcal{R}^{acc} \rrbracket_{\Sigma}^{+} \Leftrightarrow (\Lambda(\sigma_2) = \Lambda(\sigma_1) \setminus \{(s, o, a)\} \wedge \Upsilon(\sigma_1) = \Upsilon(\sigma_2))
$$
Une autre approche, plus faible, peut être utilisée pour définir la sémantique des requêtes. Cette approche nous permettra d'obtenir des résultats facilitant la comparaison de modèles de contrôle d'accès. Elle consiste en la définition d'une relation $\|\mathcal{R}\|_{\Sigma} \subseteq \mathcal{R} \times \Sigma$ telle que $(R, \sigma)$ appartient à $\|\mathcal{R}\|_{\Sigma}$, si l'état $\sigma$ a pu être obtenu en appliquant avec succès la requête $R$ (on ne tient pas compte de l'état de départ). Par exemple, une sémantique faible possible pour l'ensemble $\mathcal{R}^{acc}$ est :

$$ \begin{aligned} (\langle +, s, o, a \rangle, \sigma) \in \|\mathcal{R}\|_{\Sigma} &\Leftrightarrow (s, o, a) \in \Lambda(\sigma) \\ (\langle -, s, o, a \rangle, \sigma) \in \|\mathcal{R}\|_{\Sigma} &\Leftrightarrow (s, o, a) \notin \Lambda(\sigma) \end{aligned} $$

Cette notion de sémantique est qualifiée de sémantique faible dans le sens où elle spécifie les propriétés que doit vérifier un état après application d'une requête, et non pas les changements effectués à partir d'un état. Néanmoins, ces changements sont en partie caractérisés par un partitionnement de l'ensemble des requêtes :

$$ \mathcal{R} = \mathcal{R}^{\otimes} \cup \mathcal{R}^{\flat} \cup \mathcal{R}^{\top} $$

qui permet de spécifier la variation des accès potentiels lors de l'application des requêtes. L'ensemble $\mathcal{R}^{\otimes}$ (resp. $\mathcal{R}^{\flat}$) contient les requêtes d'élargissement (resp. rétrécissement) des accès potentiels et l'ensemble $\mathcal{R}^{\top}$ contient les autres requêtes. Autrement dit, si l'on passe d'un état $\sigma_1$ à un état $\sigma_2$ en appliquant avec succès une requête $R \in \mathcal{R}^{\otimes}$ (resp. $R \in \mathcal{R}^{\flat}$), alors l'ensemble des ensembles d'accès que l'on peut ajouter à $\sigma_2$ (resp. $\sigma_1$), sans modifier les fonctions de sécurité, est inclus dans celui des ensembles d'accès que l'on peut ajouter à $\sigma_1$ (resp. $\sigma_2$) sans modifier les fonctions de sécurité. Par exemple, pour la politique de la Muraille de Chine, la requête $\langle +, s, o, a \rangle$ appartient à l'ensemble $\mathcal{R}^{\otimes}$ étant donné qu'ajouter un accès ne permet pas d'ajouter un autre accès précédemment interdit et empêche l'ajout éventuel d'autres accès. A l'inverse, la requête $\langle -, s, o, a \rangle$ appartient à $\mathcal{R}^{\otimes}$ étant donné que le relâchement d'un accès n'empêche pas d'ajouter un accès précédemment autorisé et peut autoriser l'ajout de certains accès interdits auparavant.

Bien sûr, les deux procédés de définition d'une sémantique du langage de requêtes n'ont pas le même pouvoir d'expression, mais peuvent, dans certains cas, être reliés.

## Modèles et Implantations

La notion de modèle est définie comme suit.

**Définition 2.2** Un modèle de contrôle d'accès $M[\rho]$ est défini par une paire $M[\rho] = (\mathbb{P}[\rho], \mathcal{R})$ et par la donnée d'une sémantique pour $\mathcal{R}$.

L'implantation d'un modèle de contrôle d'accès $M[\rho]$ sous la forme d'une machine à états consiste à définir à la fois un ensemble d'états initiaux $\Sigma_I$ et une fonction de transition $\tau: \mathcal{R} \times \Sigma \to \mathcal{D} \times \Sigma$ (où $\mathcal{D} = \{\text{yes}, \text{no}\}$ est un ensemble de réponses) qui permet de passer d'un état à un autre en fonction d'une requête. Plusieurs propriétés de correction et de complétude sont définies sur les implantations. Elles sont détaillées en annexe D et concernent essentiellement la politique de contrôle d'accès appliquée (i.e. le prédicat $\Omega$) et le respect de la sémantique des requêtes. Nous notons $M[\rho] \vdash (\tau, \Sigma_I)$ lorsque toutes les propriétés de correction d'une implantation $(\tau, \Sigma_I)$ d'un modèle $M[\rho]$ sont satisfaites.

Plusieurs exemples de modèles classiques de contrôle d'accès accompagnés de leurs implantations sont formalisés en annexe D.1.2.
## 2.2 Comparaison de modèles de contrôle d'accès

Dans cette section nous présentons deux approches qui ont été utilisées pour comparer des modèles de contrôle d'accès. Intuitivement, un modèle de contrôle d'accès $M_1[\rho_1]$ est plus restrictif qu'un modèle $M_2[\rho_2]$ si et seulement si chaque implantation correcte de $M_1[\rho_1]$ peut être simulée par une implantation correcte de $M_2[\rho_2]$. Evidemment, la principale difficulté pour comparer deux modèles provient du fait qu'il est nécessaire de considérer toutes les implantations d'un modèle, ce qui, dans la pratique, est difficilement réalisable. Toutefois, nous allons voir que sous certaines hypothèses, vérifiées dans tous les exemples concrets que nous avons envisagés, il est possible de limiter le nombre d'implantations à considérer lors de la comparaison.

La première approche, détaillée en annexe D.2.1, a été utilisée pour comparer les modèles de la Muraille de Chine, de Bell et LaPadula et à base de rôles (RBAC96). La deuxième approche a été utilisée pour comparer les modèles HRU, de Bell et LaPadula et RBAC96. Elle est détaillée en annexe D.2.2.

### 2.2.1 Comparaison de modèles : Accès

#### Définition d'un préordre partiel sur les modèles

La première approche pour comparer deux modèles nécessite que ces deux modèles partagent le même ensemble de requêtes sur lequel une sémantique faible est définie. Cette approche ne permet donc pas de prendre en compte les requêtes administratives qui sont propres à chaque modèle. Cette restriction permet de considérer la notion de simulation d'implantations, définie de manière classique comme suit.

Etant données deux fonctions de transition $\tau_1 : \mathcal{R} \times \Sigma_1 \to \mathcal{D} \times \Sigma_1$ et $\tau_2 : \mathcal{R} \times \Sigma_2 \to \mathcal{D} \times \Sigma_2$, $\tau_2$ simule $\tau_1$, ce que nous notons $\tau_1 \stackrel{\kappa\Sigma}{\rightleftharpoons} \tau_2$, ssi il existe une relation $\kappa\Sigma \subseteq \Sigma_1 \times \Sigma_2$ telle que :

$$ 
\begin{array}{l}
\forall \sigma_1, \sigma'_1 \in \Sigma_1 \quad \forall \sigma_2 \in \Sigma_2 \quad \forall R \in \mathcal{R} \quad \forall a \in \mathcal{D} \\
\quad ((\sigma_1, \sigma_2) \in \kappa_{\Sigma} \wedge \tau_1(R, \sigma_1) = (a, \sigma'_1)) \\
\Rightarrow \quad (\exists \sigma'_2 \in \Sigma_2 (\sigma'_1, \sigma'_2) \in \kappa_{\Sigma} \wedge \tau_2(R, \sigma_2) = (a, \sigma'_2))
\end{array}
$$

Cette définition est étendue aux implantations : l'implantation $(\tau_2, \Sigma_I^2)$ simule l'implantation $(\tau_1, \Sigma_I^1)$, ce que nous notons $(\tau_1, \Sigma_I^1) \stackrel{\kappa\Sigma}{\rightleftharpoons} (\tau_2, \Sigma_I^2)$, ssi il existe une relation $\kappa\Sigma \subseteq \Sigma_1 \times \Sigma_2$ telle que :

$$ \tau_1 \stackrel{\kappa\Sigma}{\rightleftharpoons} \tau_2 \wedge \forall \sigma_1 \in \Sigma_I^1 \exists \sigma_2 \in \Sigma_I^2 \quad (\sigma_1, \sigma_2) \in \kappa_{\Sigma} $$

En fait, il est nécessaire de préciser la notion d'ordre entre modèles. En effet, la relation de simulation utilisée pour montrer qu'un modèle $M_1[\rho_1]$ est plus restrictif qu'un modèle $M_2[\rho_2]$ doit satisfaire de "bonnes propriétés". Par exemple, si on considère le produit cartésien $\Sigma_1 \times \Sigma_2$ comme une relation de simulation entre implantations, il devient facile d'établir que tout modèle est plus restrictif que tout autre modèle. Il faut donc contraindre la notion de relation de simulation. La définition formelle des propriétés requises pour les relations de simulation est donnée en annexe D.2.1. Nous écrirons ici $P_s(\kappa\Sigma)$ pour exprimer que la relation $\kappa\Sigma$ satisfait ces propriétés. Ces propriétés reposent sur une relation d'équivalence $\equiv_\iota$ (définie en annexe D.2.1) sur les états d'un même modèle qui permet
de caractériser les états “sémantiquement” équivalents<fnref n="3" />. De plus, nous imposons que les fonctions de transition $\tau$ considérées préservent cette relation, ce que nous notons $\equiv_\tau \tau$ (deux états équivalents sont transformés en états équivalents par $\tau$).

Ces définitions nous permettent d'introduire une relation de préordre partiel sur les modèles : un modèle $M_1[\rho_1]$ est plus restrictif qu'un modèle $M_2[\rho_2]$ ssi il existe une relation de simulation (satisfaisant de bonnes propriétés) qui permet de simuler toute implantation correcte de $M_1[\rho_1]$ par une implantation correcte de $M_2[\rho_2]$.

**Définition 2.3** Etant donnés deux modèles de contrôle d'accès $M_1[\rho_1] = (\mathbb{P}_1[\rho_1], \mathcal{R})$ et $M_2[\rho_2] = (\mathbb{P}_2[\rho_2], \mathcal{R})$ où $\mathcal{R}$ est muni d'une sémantique faible, $M_1[\rho_1] \leq M_2[\rho_2]$ ssi il existe une relation $\kappa_\Sigma \subseteq \Sigma_1 \times \Sigma_2$ telle que $P_s(\kappa_\Sigma)$ et telle que :

$$ 
\begin{array}{l}
\forall \tau_1 : \mathcal{R} \times \Sigma_1 \to \mathcal{D} \times \Sigma_1 \quad \forall \Sigma_I^1 \subseteq \Sigma_I \\
M_1[\rho_1] \vdash (\tau_1, \Sigma_I^1) \wedge \equiv_{\tau_1} \tau_1 \\
\Rightarrow \exists \tau_2 : \mathcal{R} \times \Sigma_2 \to \mathcal{D} \times \Sigma_2 \quad \exists \Sigma_I^2 \subseteq \Sigma_2 \\
M_2[\rho_2] \vdash (\tau_2, \Sigma_I^2) \wedge \equiv_{\tau_2} \tau_2 \wedge (\tau_1, \Sigma_I^1) \stackrel{\kappa_\Sigma}{\equiv} (\tau_2, \Sigma_I^2)
\end{array}
$$

Nous présentons à présent quelques moyens possibles pour réduire le nombre d'implantations à considérer lors de la comparaison de deux modèles.

## Notion de modèle réduit

La définition du préordre qui vient d'être introduite fait intervenir une relation d'équivalence $\equiv_\tau$ sur les états d'un même modèle. Cette relation préserve à la fois le prédicat de sécurité $\Omega$ et la sémantique faible des requêtes :

$$ (\sigma_1 \equiv_\tau \sigma_2 \wedge \Omega(\sigma_1)) \Rightarrow \Omega(\sigma_2) \\ \forall R \in \mathcal{R} (\sigma_1 \equiv_\tau \sigma_2 \wedge (R, \sigma_1) \in \mathbb{R}_{\Sigma}) \Rightarrow (R, \sigma_2) \in \mathbb{R}_{\Sigma} $$

Une première façon de réduire le nombre d'implantations à simuler lors de la comparaison de deux modèles consiste à considérer l'ensemble quotient $\Sigma_{\equiv_\tau}$ ce qui conduit à définir la notion de modèle réduit :

- la réduction de la politique $\mathbb{P}[\rho]$ est la politique $\mathbb{P}^\sharp[\rho] = (S, O, A, \hat{e}(\Sigma), \Omega)$,

- la réduction du modèle $M[\rho]$ est le modèle $M^\sharp[\rho] = (\mathbb{P}^\sharp[\rho], \mathcal{R})$,

où $e: \Sigma \to \Sigma$ est la fonction de projection associée à $\equiv_\tau$ permettant d'associer un élément canonique à chaque état, $\hat{e}(E) = \{e(\sigma) | \sigma \in E\}$ et $\mathcal{R}$ est muni de la relation de sémantique faible définie par $\mathbb{R}_{\hat{e}(\Sigma)} = \{(R, \sigma) \in \mathbb{R}_{\Sigma} | \sigma \in \hat{e}(\Sigma)\}$.

Ce procédé permet d'associer à toute implantation $I$ d'un modèle $M[\rho]$ une implantation $I^\sharp$ du modèle réduit $M^\sharp[\rho]$, les propriétés de correction des implantations étant conservées

<footnote n="3">³Considérons par exemple le cas où une fonction de sécurité d'un état permet d'obtenir l'heure courante, afin de pouvoir enregister dans des fichiers de "logs" chaque action effectuée ainsi que l'heure à laquelle elle a été effectuée. L'heure de l'accès est une information qui n'a aucun impact sur la politique de sécurité ou le modèle. Autrement dit, une requête est autorisée ou non indépendamment de l'heure. Dans ce cas, deux états contenant les mêmes accès et les mêmes informations de sécurité, mais deux heures différentes, peuvent être considérés comme équivalents. Nous présentons de manière plus formelle cette notion d'équivalence, notée $\equiv_\epsilon$, entre états en annexe D.</footnote>
par cette transformation. Il devient alors possible de définir un préordre partiel $\leq_{\#}$ sur les modèles réduits tel que :

$$M_1[\rho_1] \leq M_2[\rho_2] \Leftrightarrow M_1^{\#}[\rho_1] \leq_{\#} M_2^{\#}[\rho_2]$$

Ce résultat permet de comparer deux modèles entre eux en considérant leurs modèles réduits. Cette comparaison est a priori plus simple, car un modèle réduit possède moins d'implantations que le modèle à partir duquel il a été obtenu par réduction. La notion de réduction de modèles permet d'abstraire un modèle en regroupant les états équivalents selon une certaine sémantique définie par la relation d'équivalence $\equiv_t$ utilisée pour construire le modèle réduit. Notons cependant qu'en pratique, un modèle réduit n'a pas vocation à être effectivement construit (i.e. calculé par un algorithme). En effet, la notion de modèle réduit sert essentiellement à simplifier certaines preuves (en faisant abstraction d'informations "non discriminantes" au regard de la politique<fnref n="4" />). Comparer deux modèles de contrôle d'accès ne nécessite pas forcément de les réduire (on peut par exemple utiliser des résultats dont l'énoncé ne fait pas intervenir la notion de modèles réduits, bien que leurs preuves reposent fortement sur cette notion). Toutefois, la caractérisation du modèle réduit associé à un modèle permet de simplifier sa manipulation dans les raisonnements et d'en avoir une compréhension plus fine.

Quoi qu'il en soit, même en comparant des modèles réduits, le nombre d'implantations à simuler peut constituer un obstacle et nous introduisons dans la suite d'autres techniques permettant de réduire, sous certaines conditions, le nombre d'implantations à considérer.

## Préordre sur les implantations

Etant donné un modèle, plusieurs implantations correctes, plus ou moins restrictives, de ce modèle peuvent être envisagées. Ces implantations peuvent correspondre à différents modes de fonctionnement du système. Nous introduisons donc un préordre $\sqsubseteq$ sur les implantations d'un même modèle (ce préordre est défini en annexe D.2.1). Intuitivement, étant données deux implantations $I$ et $I'$, $I \sqsubseteq I'$ signifie que $I'$ permet de faire des "plus petits pas" que $I$. En d'autres termes, si $I$ permet d'atteindre un état $\sigma_1$ à partir d'un état $\sigma$, alors $\sigma_1$ est également atteignable par $I'$ à partir d'un état $\sigma_2$ qui est "plus proche" de $\sigma_1$ que $\sigma$. L'intérêt de ce préordre provient du fait qu'il permet de factoriser certaines propriétés. On montre en effet que :

- Si $I$ est une implantation correcte d'un modèle, alors toute implantation $I'$ telle que $I' \sqsubseteq I$ est correcte pour ce modèle.

- Si $I$ est une implantation simulable par une implantation d'un modèle $M[\rho]$, alors toute implantation $I'$ telle que $I' \sqsubseteq I$ est simulable par une implantation de $M[\rho]$.

Ainsi, pour prouver qu'un modèle est plus restrictif qu'un autre, il suffit de savoir simuler toute implantation $\sqsubseteq$-maximale du premier par une implantation du deuxième. Pour profiter de ce résultat en pratique, il faut cependant que toute implantation soit inférieure à une implantation maximale. Dans le cas où il existe une chaîne infinie croissante d'implantations, cette technique n'est pas applicable.

<footnote n="4">⁴Ce mécanisme de réduction revient donc à caractériser l'information non discriminante décrite par une représentation des états du système. C'est précisément cette information qui est ignorée dans le modèle réduit. Ce procédé est similaire à celui utilisé dans les techniques d'analyse statique à base d'interprétation abstraite.</footnote>
## Propriétés sur les relations de simulation

En pratique, comparer deux modèles $M_1[\rho_1]$ et $M_2[\rho_2]$ conduit souvent à définir un "plongement" de $\Sigma_1$ vers $\Sigma_2$ satisfaisant de "bonnes propriétés". On peut alors définir une relation de simulation $\kappa_\Sigma$ à partir de ce plongement. Sur les exemples concrets que nous avons envisagés, les relations obtenues satisfont de "bonnes propriétés". En effet, lors de la comparaison des modèles de la Muraille de Chine, de Bell & LaPadula et de RBAC, chaque relation $\kappa_\Sigma$ préserve à la fois les propriétés de sécurité définies par les prédicats $\Omega_1$ et $\Omega_2$, et la sémantique faible des requêtes. Lorsque la relation $\kappa_\Sigma$ satisfait ces propriétés, il est possible de montrer que $M_1[\rho_1] \leq M_2[\rho_2]$. Une fois établi, ce résultat permet donc de comparer deux modèles sans avoir à considérer les implantations de ces modèles, il suffit d'étudier les propriétés de la relation de simulation.

En adoptant cette approche, nous avons prouvé que le modèle de la Muraille de Chine est strictement plus restrictif que le modèle de Bell et LaPadula, qui est lui même strictement plus restrictif que le modèle RBAC à base de rôles.

### 2.2.2 Comparaison de modèles : Administration

Le mécanisme de comparaison présenté dans la section 2.2.1 n'est utilisable que si les deux modèles considérés partagent le même ensemble de requêtes muni d'une sémantique faible. Il ne permet donc pas la prise en compte des requêtes administratives permettant de modifier les informations de sécurité du système. Dans cette section, nous étendons ce mécanisme de comparaison afin de pouvoir comparer deux modèles lorsqu'ils ne partagent pas le même ensemble de requêtes. Pour ce faire, le préordre sur les modèles que nous introduisons repose sur la définition d'une relation mettant en correspondance les (séquences de) requêtes "sémantiquement" équivalentes des deux modèles et sur la notion de simulation faible qui permet la simulation d'une transition par une séquence de transitions. En effet, selon le pouvoir d'expression des deux langages de requêtes considérés $R_1$ et $R_2$, il se peut que pour simuler l'effet d'une requête appartenant à $R_1$, il soit nécessaire d'appliquer plusieurs requêtes de $R_2$. Comme nous le verrons, c'est par exemple le cas pour la requête d'ajout d'un rôle autorisé pour un utilisateur dans le modèle RBAC, dont la simulation dans le modèle HRU nécessite d'ajouter plusieurs accès autorisés et donc d'appliquer plusieurs fois la requête du modèle HRU permettant d'autoriser un nouvel accès.

#### Langage de requêtes

L'ensemble $\mathcal{R}$ des requêtes d'un modèle de contrôle d'accès peut se décomposer en trois sous-ensembles :

$$ \mathcal{R} = \mathcal{R}^{acc} \cup \mathcal{R}^{adm} \cup \{Success, Fail\} $$

où $\mathcal{R}^{acc}$ est l'ensemble défini en (2.1), $\mathcal{R}^{adm}$ contient les requêtes administratives du modèle et *Success* et *Fail* sont des requêtes ne produisant aucun effet mais qui seront utiles pour envisager la simulation faible d'implantations. La sémantique des requêtes de $\mathcal{R}$ est définie via une relation $\llbracket \mathcal{R} \rrbracket_\Sigma^+ \subseteq \Sigma \times \mathcal{R} \times \Sigma$. La sémantique des requêtes appartenant à $\mathcal{R}^{acc}$ a déjà été introduite page 24, celle des requêtes appartenant à $\mathcal{R}^{adm}$ dépend du modèle considéré
et la sémantique des requêtes *Success* et *Fail* est définie par :

$$ (\sigma_1, \text{Success}, \sigma_2) \in \mathbb{R}_{\Sigma}^{+} \Leftrightarrow (\Lambda(\sigma_1) = \Lambda(\sigma_2) \wedge \Upsilon(\sigma_1) = \Upsilon(\sigma_2)) \\ (\sigma_1, \text{Fail}, \sigma_2) \in \mathbb{R}_{\Sigma}^{+} \Leftrightarrow (\Lambda(\sigma_1) = \Lambda(\sigma_2) \wedge \Upsilon(\sigma_1) = \Upsilon(\sigma_2)) $$

Toutes les fonctions de transition que nous considérons dans cette section doivent vérifier les propriétés suivantes : les requêtes *Success* et *Fail* ne modifient pas les états, la requête *Success* est toujours acceptée, la requête *Fail* est toujours refusée, et si une requête est refusée alors l'état n'est pas modifié.

$$ \forall \sigma \in \Sigma \quad \tau(\text{Success}, \sigma) = (\text{yes}, \sigma) \wedge \tau(\text{Fail}, \sigma) = (\text{no}, \sigma) \\ \forall \sigma_1, \sigma_2 \in \Sigma \quad \forall R \in \mathcal{R} \quad \tau(R, \sigma_1) = (\text{no}, \sigma_2) \Rightarrow \sigma_1 = \sigma_2 $$

## Définition d'un préordre partiel sur les modèles

Prendre en compte les requêtes administratives lors de la comparaison de modèles amène à la notion de simulation faible d'implantations, définie comme suit. Etant données deux fonctions de transition $\tau_1 : \mathcal{R}_1 \times \Sigma_1 \to \mathcal{D} \times \Sigma_1$ et $\tau_2 : \mathcal{R}_2 \times \Sigma_2 \to \mathcal{D} \times \Sigma_2$, $\tau_2$ simule faiblement $\tau_1$, ce que nous notons $\tau_1 \xrightarrow{\kappa_{\Sigma}, \kappa_{\mathcal{R}}} \tau_2$, ssi il existe deux relations $\kappa_{\Sigma} \subseteq \Sigma_1 \times \Sigma_2$ et $\kappa_{\mathcal{R}} \subseteq \Sigma_1 \times \mathcal{R}_1 \times \mathcal{R}_2^*$ telles que :

$$ \forall \sigma_1, \sigma'_1 \in \Sigma_1 \quad \forall \sigma_2^0 \in \Sigma_2 \quad \forall R_1 \in \mathcal{R}_1 \quad \forall d_1 \in \mathcal{D} \quad \left( \begin{array}{l} \exists \sigma_2^1, \sigma_2^2, \dots, \sigma_2^{n-1}, \sigma_2^n \in \Sigma_2 \\ \exists (R_2^1, \dots, R_2^n) \in \mathcal{R}_2^* \exists d_2^1, \dots, d_2^n \in \mathcal{D} \\ \tau_2(R_2^1, \sigma_2^0) = (d_2^1, \sigma_2^1) \\ \wedge \quad \dots \wedge \tau_2(R_2^n, \sigma_2^{n-1}) = (d_2^n, \sigma_2^n) \\ \wedge \quad d_1 = d_2^1 = d_2^2 = \dots = d_2^n \\ \wedge \quad (\sigma_1, R_1, (R_2^1, \dots, R_2^n)) \in \kappa_{\mathcal{R}} \\ \wedge \quad (\sigma'_1, \sigma'_2) \in \kappa_{\Sigma} \end{array} \right) \\ \Rightarrow \quad \left( \begin{array}{l} \tau_1(R_1, \sigma_1) = (d_1, \sigma'_1) \\ \wedge \quad (\sigma_1, \sigma_2^0) \in \kappa_{\Sigma} \end{array} \right) $$

Chaque transition de $\tau_1$ doit donc pouvoir être simulée par une séquence de transitions de $\tau_2$. Cette définition, illustrée sur la figure 2.1, est étendue aux implantations : l'implantation $(\tau_2, \Sigma_1^I)$ simule faiblement $(\tau_1, \Sigma_1^I)$, ce que nous notons $(\tau_1, \Sigma_1^I) \xrightarrow{\kappa_{\Sigma}, \kappa_{\mathcal{R}}} (\tau_2, \Sigma_2^I)$, ssi il existe deux relations $\kappa_{\Sigma} \subseteq \Sigma_1 \times \Sigma_2$ et $\kappa_{\mathcal{R}} \subseteq \Sigma_1 \times \mathcal{R}_1 \times \mathcal{R}_2^*$ telles que :

$$ \tau_1 \xrightarrow{\kappa_{\Sigma}, \kappa_{\mathcal{R}}} \tau_2 \wedge \forall \sigma_1 \in \Sigma_1^I \exists \sigma_2 \in \Sigma_2^I (\sigma_1, \sigma_2) \in \kappa_{\Sigma} $$

Remarquons ici que la relation $\kappa_{\mathcal{R}}$ est une relation ternaire. Le jugement $(\sigma, R_1, (R_2^1, \dots, R_2^n))$ exprime que la séquence de requêtes $(R_2^1, \dots, R_2^n)$ simule la requête $R_1$ lorsque le système se trouve dans un état $\sigma$. En effet, la séquence de requêtes peut dépendre de l'état dans lequel se trouve le système. C'est par exemple le cas pour la requête d'ajout d'une permission $(o, a)$ à un rôle $r$ dans le modèle RBAC, dont la simulation dans le modèle HRU nécessite d'ajouter les accès $(s, o, a)$ aux accès autorisés pour chaque sujet $s$ ayant activé un rôle $r'$ supérieur à $r$. Ici, l'ensemble des rôles activés par un sujet est défini par une fonction de sécurité, qui dépend donc de l'état du système.

Ici encore, les relations $\kappa_{\Sigma}$ et $\kappa_{\mathcal{R}}$ utilisables pour montrer les propriétés de simulation qui interviennent dans la définition du préordre sur les modèles doivent satisfaire certaines conditions. Il s'agit essentiellement de garantir que l'équivalence "sémantique" entre états
<figure><img src="image_9.png" /><figcaption>FIG. 2.1 – Simulation faible</figcaption></figure>

induite par la relation $\kappa_{\Sigma}$ est préservée lors de la simulation faible. Plus formellement, nous imposons que $\kappa_{\Sigma}$ soit $W$-préservante :

$$ \forall \sigma_1 \in \Sigma_1 \quad \forall \sigma_2 \in \Sigma_2 \quad (\sigma_1, \sigma_2) \in \kappa_{\Sigma} \Rightarrow W(\sigma_1) = W(\sigma_2) $$

Ces définitions nous permettent d'introduire la relation de préordre partiel suivante sur les modèles de contrôle d'accès : un modèle $M_1[\rho_1]$ est plus restrictif qu'un modèle $M_2[\rho_2]$ ssi pour toute implantation correcte $I_1$ de $M_1[\rho_1]$, il existe deux relations $\kappa_{\Sigma}$ et $\kappa_{\mathcal{R}}$ (satisfaisant de bonnes propriétés) qui permettent de simuler $I_1$ par une implantation correcte de $M_2[\rho_2]$.

**Définition 2.4** Soient $M_1[\rho_1] = (\mathbb{P}_1[\rho_1], \mathcal{R}_1)$ et $M_2[\rho_2] = (\mathbb{P}_2[\rho_2], \mathcal{R}_2)$ deux modèles.

$$ M_1[\rho_1] \leq M_2[\rho_2] $$

$$ \Leftrightarrow \left( \begin{array}{l} \forall \tau_1 : \mathcal{R}_1 \times \Sigma_1 \to \mathcal{D} \times \Sigma_1 \quad \forall \Sigma_1^I \subseteq \Sigma_1 \\ \mathbb{M}_1[\rho_1] \vdash (\tau_1, \Sigma_1^I) \Rightarrow \left( \begin{array}{l} \exists \tau_2 : \mathcal{R}_2 \times \Sigma_2 \to \mathcal{D} \times \Sigma_2 \quad \exists \Sigma_2^I \subseteq \Sigma_2 \\ \exists \kappa_{\Sigma} \subseteq \Sigma_1 \times \Sigma_2 \exists \kappa_{\mathcal{R}} \subseteq \Sigma_1 \times \mathcal{R}_1 \times \mathcal{R}_2^* \\ \kappa_{\Sigma} \text{ et } \kappa_{\mathcal{R}} \text{ sont totales à gauche} \\ \wedge \kappa_{\Sigma} \text{ est W-préservante} \\ \wedge M_2[\rho_2] \vdash (\tau_2, \Sigma_2^I) \wedge (\tau_1, \Sigma_1^I) \xrightarrow{\kappa_{\Sigma}, \kappa_{\mathcal{R}}} (\tau_2, \Sigma_2^I) \end{array} \right) \end{array} \right) $$

Remarquons que la comparaison de deux modèles $M_1[\rho_1]$ et $M_2[\rho_2]$ selon la relation $\leq$ nécessite la construction d'une relation de simulation qui permet de simuler toutes les implantations correctes de $M_1[\rho_1]$ par des implantations correctes de $M_2[\rho_2]$, alors que la comparaison de $M_1[\rho_1]$ et $M_2[\rho_2]$ selon la relation $\leq$ nécessite la construction d'une relation de simulation pour chaque implantation correcte de $M_1[\rho_1]$. Toutefois, en pratique, les relations $\kappa_{\Sigma}$ et $\kappa_{\mathcal{R}}$ sont définies indépendamment de l'implantation considérée et il suffit alors de restreindre $\kappa_{\mathcal{R}}$ en fonction de la fonction de transition à simuler.

## Propriétés sur les relations de simulation

Sur les exemples que nous avons considérés, les relations $\kappa_{\Sigma}$ et $\kappa_{\mathcal{R}}$ satisfont de "bonnes propriétés" : ces relations préservent à la fois les propriétés de sécurité définies par les
prédicats $\Omega_1$ et $\Omega_2$, et la sémantique des requêtes. Dans ce cas, il est possible de montrer que $M_1[\rho_1] \subseteq M_2[\rho_2]$. Une fois établi, ce résultat permet donc de comparer deux modèles sans avoir à considerer les implantations de ces modèles, il suffit d'étudier les propriétés des relations $\kappa\Sigma$ et $\kappa_R$.

## 2.3 Analyse de flots d'information

Une politique de contrôle d'accès permet de spécifier quels sont les accès autorisés lorsque le système se trouve dans un certain état mais ne permet pas, tout du moins de manière explicite, de spécifier les flots d'information qui sont autorisés durant la vie du système. Ainsi, une fois qu'un sujet a pu accéder à un objet, il n'y a généralement aucun contrôle sur la propagation de l'information lue par le sujet. Par exemple, avec un modèle discrétionnaire, il est possible qu'un sujet $s_1$ lise un objet $o_1$ et recopie l'information lue dans un objet $o_2$ accessible en lecture par un sujet $s_2$ non autorisé à lire $o_1$. La politique de contrôle d'accès est ici respectée mais ne coïncide pas avec son interprétation en termes de flots d'information. Dans cette section nous étudions la cohérence entre ces deux lec- tures sémantiques des modèles de contrôle d'accès et introduisons les concepts utiles pour analyser les flots d'information engendrés par les exécutions des implantations de modèles de contrôle d'accès.

### 2.3.1 Flots et Politiques de Flots

Nous étudions ici les flots d'information qui se produisent entre les entités du système. Nous distinguons donc les flots entre objets, entre sujets et entre sujets et objets. Pour cela, nous introduisons les notations suivantes :

- Nous notons $\hookrightarrow^{OO}$ le produit cartésien $\mathcal{O} \times \mathcal{O}$. Un élément $o_1 \hookrightarrow^{OO} o_2$ de $\mathcal{O} \times \mathcal{O}$ permet d'exprimer que le contenu d'un objet $o_1$ est propagé dans un objet $o_2$. Nous caractériserons par la suite plusieurs sous-ensembles de $\hookrightarrow^{OO}$ permettant de décrire des flots d'information entre objets dans différents contextes. Une politique de confinement est un sous-ensemble $\sim^{OO}$ de $\hookrightarrow^{OO}$.

- Nous notons $\hookrightarrow^{OS}$ le produit cartésien $\mathcal{O} \times \mathcal{S}$. Un élément $o \hookrightarrow^{OS} s$ de $\mathcal{O} \times \mathcal{S}$ permet d'exprimer qu'un sujet $s$ prend connaissance des informations contenues dans un objet $o$. Nous caractériserons par la suite plusieurs sous-ensembles de $\hookrightarrow^{OS}$ permettant de décrire des flots d'information des objets vers les sujets dans différents contextes. Une politique de confidentialité est un sous-ensemble $\sim^{OS}$ de $\hookrightarrow^{OS}$.

- Nous notons $\hookrightarrow^{SO}$ le produit cartésien $\mathcal{S} \times \mathcal{O}$. Un élément $s \hookrightarrow^{SO} o$ de $\mathcal{S} \times \mathcal{O}$ permet d'exprimer qu'un sujet $s$ propage les informations dont il dispose dans un objet $o$. Nous caractériserons par la suite plusieurs sous-ensembles de $\hookrightarrow^{SO}$ permettant de décrire des flots d'information des sujets vers les objets dans différents contextes. Une politique d'intégrité est un sous-ensemble $\sim^{SO}$ de $\hookrightarrow^{SO}$.

- Nous notons $\hookrightarrow^{SS}$ le produit cartésien $\mathcal{S} \times \mathcal{S}$. Un élément $s_1 \hookrightarrow^{SS} s_2$ de $\mathcal{S} \times \mathcal{S}$ permet d'exprimer qu'un sujet $s_1$ rend accessibles les informations dont il dispose à un sujet $s_2$. Nous caractériserons par la suite plusieurs sous-ensembles de $\hookrightarrow^{SS}$ permettant de décrire des flots d'information entre sujets dans différents contextes.
<figure><img src="image_10.png" /><figcaption>FIG. 2.2 – Flots d’information</figcaption></figure>

Flots d'information engendrés par une séquence d'états

Les flots d'information créés durant la vie d'un système sont caractérisés à partir d'une séquence d'états décrivant les états successifs du système. A partir de l'ensemble des accès courants qui ont lieu lorsque le système se trouve dans un état $\sigma$, nous pouvons définir les flots d'information entre objets comme suit. Le contenu d'un objet $o_1$ est diffusé dans un objet $o_2$ s'il existe un ensemble de sujets dont les accès sur les objets du système permettent de recopier l'information de $o_1$ dans $o_2$, cette information pouvant transiter par des objets intermédiaires :

$$ \left\{ \left( \bigwedge_{o_1 \hookrightarrow \mathcal{O}} \left( \bigwedge_{o_2 \hookrightarrow \mathcal{O}} \left( \begin{array}{l} \exists s_1, \dots, s_k, s_{k+1} \in \mathcal{S} \ \exists o^1, \dots, o^k \in \mathcal{O} \\ \left( \begin{array}{l} (s_1, o_1, \text{read}), (s_1, o^1, \text{write}), \\ (s_2, o^1, \text{read}), (s_2, o^2, \text{write}), \\ \vdots, \\ (s_i, o^{i-1}, \text{read}), (s_i, o^i, \text{write}), \\ \vdots, \\ (s_{k+1}, o^k, \text{read}), (s_{k+1}, o_2, \text{write}) \end{array} \right) \subseteq \Lambda(\sigma) \\ \lor o_1 = o_2 \end{array} \right) \right) \right\} $$

Cette définition, illustrée sur la partie gauche de la figure 2.2, peut être étendue à un ensemble d'états $E \subseteq \Sigma : \hookrightarrow_{\mathcal{E}}^{\mathcal{O}} = \bigcup_{\sigma \in E} \hookrightarrow_{\sigma}^{\mathcal{O}}$.

Nous pouvons à présent définir les flots d'information qui ont lieu durant une séquence d'états $(\sigma_1, \dots, \sigma_n)$ :
- Les flots entre objets sont obtenus par composition des flots engendrés par chacun des états apparaissant dans la séquence :

$$ \leftarrow_{(\sigma_1, \dots, \sigma_n)}^{\mathrm{OO}} = \left\{ \begin{array}{ll} \leftarrow_{\sigma_1}^{\mathrm{OO}} & \text{si } n=1 \\ \leftarrow_{\sigma_{k+1}}^{\mathrm{OO}} \circ \leftarrow_{(\sigma_1, \dots, \sigma_k)}^{\mathrm{OO}} & \text{si } n=k+1 \end{array} \right. $$

- Les flots d'un objet o vers un sujet s sont identifiés lorsqu'un objet o' a reçu l'information contenue dans o et que s accède ensuite en lecture à o' :

$$ \leftarrow_{(\sigma_1, \dots, \sigma_n)}^{\mathrm{OS}} = \bigcup_{i=1}^{n} \left\{ o_2 \leftarrow^{\mathrm{OS}} s \mid o_2 \leftarrow_{(\sigma_1, \dots, \sigma_i)}^{\mathrm{OO}} o_1 \wedge (s, o_1, \mathbf{read}) \in \Lambda(\sigma_i) \right\} $$

- Les flots d'un sujet s vers un objet o sont identifiés lorsque s accède en écriture à un objet o' dont le contenu est ensuite diffusé dans o :

$$ \leftarrow_{(\sigma_1, \dots, \sigma_n)}^{\mathrm{SO}} = \bigcup_{i=1}^{n} \left\{ s \leftarrow^{\mathrm{SO}} o_2 \mid (s, o_1, \mathbf{write}) \in \Lambda(\sigma_i) \wedge o_1 \leftarrow_{(\sigma_i, \sigma_{i+1}, \dots, \sigma_n)}^{\mathrm{OO}} o_2 \right\} $$

- Les flots d'un sujet s₁ vers un sujet s₂ sont identifiés lorsque s₁ écrit dans un objet dont le contenu est ensuite diffusé dans un objet qui est ensuite accédé en lecture par s₂ :

$$ \leftarrow_{(\sigma_1, \dots, \sigma_n)}^{\mathrm{SS}} = \bigcup_{i=1}^{n} \left( \leftarrow_{(\sigma_i, \dots, \sigma_n)}^{\mathrm{OS}} \circ \leftarrow_{(\sigma_1, \dots, \sigma_i)}^{\mathrm{SO}} \right) $$

Ces définitions, illustrées sur la partie droite de la figure 2.2, sont étendues aux ensembles d'états et aux ensembles de séquences d'états. Si $E \subseteq \Sigma$ est un ensemble d'états et $F \subseteq E^*$ est un ensemble de séquences d'états, on définit :

$$ \leftarrow_{Y}^{X} = \bigcup_{y \in Y} \leftarrow_{y}^{X} $$

où $X \in \{\mathrm{OO}, \mathrm{OS}, \mathrm{SO}, \mathrm{SS}\}$ et $Y \in \{E, F\}$.

Nous venons de caractériser formellement les flots d'information qui se produisent entre les entités du système durant la vie de ce système. Il est maintenant possible de comparer ces ensembles de flots avec les flots autorisés par une politique de confidentialité $\rightsquigarrow^{\mathrm{OS}}$ et une politique d'intégrité $\rightsquigarrow^{\mathrm{SO}}$. Un ensemble $X$, correspondant soit à un ensemble d'états ($X = E$), soit à un ensemble de séquences d'états ($X = F$), est :

- correct pour $\rightsquigarrow^{\mathrm{OS}}$ (resp. pour $\rightsquigarrow^{\mathrm{SO}}$) ssi $\leftarrow_{X}^{\mathrm{OS}} \subseteq \rightsquigarrow^{\mathrm{OS}}$ (resp. $\leftarrow_{X}^{\mathrm{SO}} \subseteq \rightsquigarrow^{\mathrm{SO}}$).

- complet pour $\rightsquigarrow^{\mathrm{OS}}$ (resp. pour $\rightsquigarrow^{\mathrm{SO}}$) ssi $\rightsquigarrow_{X}^{\mathrm{OS}} \subseteq \leftarrow_{X}^{\mathrm{OS}}$ (resp. $\rightsquigarrow_{X}^{\mathrm{SO}} \subseteq \leftarrow_{X}^{\mathrm{SO}}$).

La propriété de correction exprime que tous les flots engendrés par $X$ sont autorisés par la politique et la propriété de complétude exprime que tous les flots autorisés par la politique sont "réalisables" par $X$.

## Politiques de flots induites par une politique de contrôle d'accès

Une politique de contrôle d'accès $\mathbb{P}[\rho] = (S, O, A, \Sigma, \Omega)$ peut être interprétée par une politique de confidentialité et/ou une politique d'intégrité. Exprimées en termes de flots d'information, ces politiques sont définies comme suit :

$$ \rightsquigarrow_{\mathbb{P}[\rho]}^{\mathrm{OS}} = \{ o \leftarrow^{\mathrm{OS}} s \mid \exists \sigma \in \Sigma |_{\Omega} (s, o, \mathbf{read}) \in \Lambda(\sigma) \} $$

$$ \rightsquigarrow_{\mathbb{P}[\rho]}^{\mathrm{SO}} = \{ s \leftarrow^{\mathrm{SO}} o \mid \exists \sigma \in \Sigma |_{\Omega} (s, o, \mathbf{write}) \in \Lambda(\sigma) \} $$
Ainsi, $o \rightsquigarrow_{\mathbb{F}[\rho]}^{\mathrm{OS}} s$ signifie que pour un état sûr du système, le sujet $s$ accède à l'information contenue dans l'objet $o$ et $s \rightsquigarrow_{\mathbb{F}[\rho]}^{\mathrm{SO}} o$ signifie que pour un état sûr du système, le sujet $s$ propage l'information dont il dispose dans l'objet $o$.

### 2.3.2 Mécanismes de détection de flots

Les définitions introduites ci-dessus permettent d'étudier la cohérence entre les flots engendrés par les exécutions des implantations d'un modèle de contrôle d'accès et les politiques de confidentialité et d'intégrité induites par la politique de contrôle d'accès. La section D.3 en annexe présente en détail une analyse de flots pour les modèles HRU et de Bell et LaPadula. Pour certains modèles, comme celui de HRU, certaines séquences d'états, respectant la politique de contrôle d'accès, engendrent des flots non autorisés par les politiques de confidentialité et d'intégrité induites par cette politique. Dans ce cas, il peut être utile de compléter le mécanisme de contrôle d'accès à l'aide d'un mécanisme de détection de flots. Nous donnons ici la spécification formelle d'un tel mécanisme. La section D.3 en annexe présente un exemple de mécanisme de détection de flots défini dans ce formalisme. Il s'agit d'une formalisation d'un système de détection d'intrusion, décrit dans [55, 54], dont nous illustrons l'utilisation pour le modèle HRU.

#### Détection de flots

Etant donné un ensemble de flots $\rightsquigarrow_{\mathbb{F}}$, détecter les flots appartenant à $\rightsquigarrow_{\mathbb{F}}$ lors de la vie d'un système consiste à observer les séquences d'états du système et à collecter des informations permettant d'identifier celles d'entre elles qui engendrent des flots recherchés. Chaque état $\sigma$ est donc associé à une information $\psi(\sigma)$ qui rend compte d'une partie du passé de cet état. C'est à partir de cette information que l'on peut définir un prédicat $\mathcal{U}$ sur $\Sigma$ permettant de caractériser les états issus de séquences d'états engendrant un flot appartenant à $\rightsquigarrow_{\mathbb{F}}$. Ces états sont appelés des états d'alerte et on note $\Sigma|_{\mathcal{U}}$ l'ensemble $\{\sigma \in \Sigma | \mathcal{U}(\sigma)\}$. Etant donnés un ensemble $E$ d'états observables et un ensemble $F \subseteq E^*$ de séquences d'états qui peuvent se produire, un mécanisme de détection de flots est défini par :

$$ \mathbb{F}[\rho, E, F, \rightsquigarrow_{\mathbb{F}}] = (\Sigma, \mathcal{U}) $$

Bien sûr, il faut s'assurer que le prédicat $\mathcal{U}$ caractérise bien les états issus d'une séquence produisant un flot dans $\rightsquigarrow_{\mathbb{F}}$. Pour cela, nous introduisons les deux propriétés suivantes. $\mathbb{F}[\rho, E, F, \rightsquigarrow_{\mathbb{F}}] = (\Sigma, \mathcal{U})$ est :

- correct ssi tout état d'alerte est issu d'une séquence engendrant un flot dans $\rightsquigarrow_{\mathbb{F}}$ :

$$ \forall (\sigma_1, \dots, \sigma_n) \in F \quad \mathcal{U}(\sigma_n) \Rightarrow \leftarrow_{(\sigma_1, \dots, \sigma_n)}^X \cap \rightsquigarrow_{\mathbb{F}} \neq \emptyset $$

- complet ssi tout état issu d'une séquence engendrant un flot dans $\rightsquigarrow_{\mathbb{F}}$ est un état d'alerte :

$$ \forall (\sigma_1, \dots, \sigma_n) \in F \quad \leftarrow_{(\sigma_1, \dots, \sigma_n)}^X \cap \rightsquigarrow_{\mathbb{F}} \neq \emptyset \Rightarrow \mathcal{U}(\sigma_n) $$

où $X \in \{\mathrm{OO}, \mathrm{OS}, \mathrm{SO}\}$.
## Detection de flots illégaux

Un mécanisme de détection de flots $\mathbb{F}[\rho, E, F, \rightsquigarrow_{\mathbb{F}}]$ peut être utilisé pour s'assurer qu'une politique de flots $\rightsquigarrow$ est bien respectée. Dans ce cas, ce mécanisme est dit :

- correct pour $\rightsquigarrow$ ssi : $\rightsquigarrow_{\mathbb{F}} \cap \rightsquigarrow = \emptyset$

Si $\mathbb{F}[\rho, E, F, \rightsquigarrow_{\mathbb{F}}]$ est de plus correct, alors tout état d'alerte est issu d'une séquence engendrant un flot qui ne respecte pas la politique $\rightsquigarrow$.

- complet pour $\rightsquigarrow$ ssi : $(\leftarrow_X^\top \setminus \rightsquigarrow) = \rightsquigarrow_{\mathbb{F}}$

Si $\mathbb{F}[\rho, E, F, \rightsquigarrow_{\mathbb{F}}]$ est de plus complet, alors tout état issu d'une séquence engendrant un flot ne respectant pas la politique $\rightsquigarrow$ est un état d'alerte.

Muni de ce formalisme, nous pouvons montrer que lorsque nous obtenons un état d'alerte, alors soit le mécanisme de détection de flots n'est pas correct, soit il n'est pas correct pour la politique de flots considérée, soit il est issu d'une séquence engendrant un flot non autorisé par la politique de flots.

**Proposition 2.1** *Soit $\mathbb{F}[\rho, E, F, \rightsquigarrow_{\mathbb{F}}] = (\Sigma, \mathcal{U})$ un mécanisme de détection de flots et $\rightsquigarrow$ une politique de flots. Si $\leftarrow_X^\top \subseteq \rightsquigarrow$ (où $X \in \{OO, OS, SO\}$) et si $\mathbb{F}[\rho, E, F, \rightsquigarrow_{\mathbb{F}}]$ est correct et correct pour $\rightsquigarrow$, alors $E \cap \Sigma_{|\mathcal{U}} = \emptyset$.*

## 2.4 Analyse de modèles de contrôle d'accès

Dans ce chapitre nous avons introduit un cadre formel permettant de définir a priori n'importe quel modèle de contrôle d'accès, et fournissant les outils nécessaires pour comparer deux modèles entre eux et analyser les flots d'information que les exécutions de leurs implantations engendrent (implicitly). Nous avons donc défini un cadre uniforme permettant la définition de modèles de contrôle d'accès : nous avons identifié les "ingrédients" communs aux politiques de contrôle d'accès, exprimé les propriétés génériques qu'ils vérifient, prouvé certaines et formalisé les politiques envisagées comme des instances du cadre générique. Ce cadre différencie la notion de politique de contrôle d'accès de celle de modèle de contrôle d'accès. Une politique est la spécification du "quoi", dans le sens où elle définit quelles sont les entités et quels sont les états (sûrs et non sûrs). Un modèle est la spécification du "comment", dans le sens où il décrit comment passer d'un état à un autre. Plusieurs techniques de comparaison ont été introduites. Tout d'abord, une relation de préordre a été définie sur les implantations d'un modèle. Cette relation correspond à une notion de restriction : intuitivement, l'implantation la plus petite d'un modèle est celle qui permet de faire le moins de choses. Conjointement à la notion de modèle, nous avons introduit la notion de modèle réduit, qui s'obtient en ignorant l'information "inutile", c'est-à-dire l'information non discriminante au regard de la politique de sécurité. Nous avons également proposé deux préordres sur les modèles permettant de comparer formellement deux modèles de contrôle d'accès. Ces préordres expriment une notion intuitive de "plongement" : un modèle est plus restrictif qu'un autre modèle si toute implantation du premier est simulable par une implantation du deuxième. Nous avons enfin établi des résultats permettant de comparer deux modèles sans avoir à considérer toutes leurs implantations.

Quelques travaux ont déjà eu lieu sur la comparaison de modèles de contrôle d'accès mais ils sont encore parcellaires : [122] envisage la comparaison de politiques de contrôle
d'accès en termes de puissance d'expression, [23] utilise des techniques de simulation pour
comparer des modèles de contrôle d'accès discrétionnaire, [123] envisage la comparaison de
politiques sous l'angle de la combinaison de politiques. Chacune de ces approches adopte
un point de vue différent sur la notion de contrôle d'accès et il est difficile de les comparer
directement. Notons toutefois que la plupart de ces approches abordent principalement la
comparaison de modèles discrétionnaires et ne distinguent pas la sémantique des requêtes
des fonctions de transition qui permettent d'appliquer ces requêtes comme nous le faisons.
Elles sous-entendent donc que les politiques sont mises en œuvre de la manière la moins
restrictive possible (au sens de la relation $\subseteq$ introduite dans cet article). D'autre part,
lorsqu'elles prennent en compte les requêtes administratives lors de la comparaison, ces
approches ne permettent pas que la relation $\kappa_R$ dépende de l'état du système et sont
donc très restrictives. Quoi qu'il en soit, toutes ces approches portent sur le même objet
et méritent d'être reconsidérées et étendues dans un cadre uniforme afin d'en étudier les
liens et d'en dégager de nouvelles techniques de réutilisation. Cette étude permettrait
donc d'outiller (ou d'enrichir) le cadre sémantique proposé ici pour prendre en compte ces
approches.

Plusieurs mécanismes peuvent être envisagés pour garantir que les accès effectués dans
un système d’information respectent la politique de sécurité souhaitée. Usuellement, on se
ramène à :

- la mise en œuvre d'un moniteur de référence qui filtre les accès pour ne permettre
que ceux qui ne violent pas la politique de sécurité,

- la mise en œuvre d'un système de détection d'intrusion qui repose sur l'observation
des transferts d'information qui ont lieu dans le système et qui lève une alerte en cas
de transfert "suspect".

Le premier moyen est une approche défensive puisqu'aucun accès non autorisé n'est pos-
sible, tandis que le second relève d'une approche préventive puisqu'elle se contente de lever
un alerte en cas de doute. Généralement, ces deux mécanismes n'opèrent pas au même
niveau : un moniteur de référence est habituellement défini et implanté dans un langage
de haut niveau et peut être vu comme une application, tandis qu'un système de détection
d'intrusion peut opérer au niveau du système d'exploitation en observant les transferts
d'information engendrés lors de l'exécution d'un programme applicatif. Quoi qu'il en soit,
ces deux approches ont pour vocation de garantir des propriétés de confidentialité et/ou
d'intégrité sur les données d'un système d'information et partagent donc un ensemble de
spécifications. Dans ce chapitre, nous avons étudié les liens qui existent entre ces deux
mécanismes. Nous avons donc présenté une analyse des flots d'information associés à un
modèle de contrôle d'accès. Il s'agit ici d'une interprétation de la notion de politique de
contrôle d'accès différente de celle qui est implantée par un moniteur de référence. En effet,
une politique de contrôle d'accès ne fournit généralement pas explicitement de propriétés
sur la dissémination des informations dans le système et afin de garantir qu'une certaine
politique de flots est respectée, il peut être utile d'adjoindre un mécanisme de détection de
flots au moniteur de référence.

Une importante littérature sur les flots d'information existe. Dans [32], D.E. Denning
introduit une notion de modèle de flots d'information et présente dans [33] un procédé de
transformation de politiques de flots, satisfaisant certaines conditions, en une politique de
flots ayant une structure de treillis (et pouvant donc être mise en œuvre par une politique
de contrôle d'accès à la Bell et LaPadula). Dans [34], D.E. Denning utilise ce même modèle pour définir un mécanisme de certification de programmes garantissant des propriétés sur les flots engendrés lors de l'exécution de programmes. Dans [43], S.N. Foley introduit un modèle de flots permettant de prendre en compte des politiques de flots non nécessairement transitives et illustre l'intérêt d'un tel modèle sur des exemples concrets. Les liens entre modèles de contrôle d'accès et modèles de contrôle de flots ont également été étudiés. Dans [90], J. McLean introduit une théorie des flots d'information afin de définir un modèle de sécurité à base de flots. Dans [99], S.L. Osborn décrit comment caractériser les flots possibles dans un système RBAC à partir des paramètres de sécurité de ce système. Plus récemment, dans [9] les auteurs formalisent la notion de DTE (Domain Type Enforcement) [10] afin de fournir un mécanisme de contrôle de flots qu'ils intègrent ensuite dans le modèle OrBAC (Organization based access control model) [73]. Ici encore, tous ces travaux portent sur des notions communes et il serait intéressant de les exprimer dans notre formalisme afin de pouvoir analyser leurs points communs et leurs différences, de comparer leur pouvoir d'expression et de comprendre comment une implantation de l'un de ces modèles peut être étendue pour inclure les particularités d'un autre modèle.
Conclusion – Perspectives

Les travaux présentés dans ce document débutent tous par une description formelle du domaine étudié. A chaque fois, la formalisation entreprise a permis d'éclairer certains points obscurs.

- En obligeant à examiner de manière très approfondie les différents aspects et composants de l'objet formalisé. C'est le cas par exemple du domaine du contrôle d'accès.

- En suscitant l'expression de certaines hypothèses restées implicites et de certaines propriétés indispensables pour établir la preuve de propriétés souhaitées. Ce fût par exemple le cas lors de la formalisation des résultats classiques de la programmation logique.

- En permettant la détection et la correction de certaines erreurs. Cela a été le cas lors de la formalisation des propriétés de sécurité de la politique de Bell et LaPadula exprimées de manière informelle, ou encore lors de la mécanisation de la preuve de complétude de la SLD-résolution.

De plus, l'ensemble des formalisations effectuées a permis de dégager des méthodes permettant une réutilisation plus aisée de développements formels. Enfin, puisque l'activité de formalisation permet de mieux comprendre l'objet formalisé, il nous a semblé naturel d'adopter cette démarche dans certaines activités d'enseignement. L'article [30] présente une expérience d'enseignement de la sémantique en utilisant le système Coq et l'atelier Focal.

Le domaine principalement abordé dans ce document est celui de la sécurité, sur lequel nous travaillons depuis 2003 et plus particulièrement de la sécurité au niveau accès. Il s'agit ici de régir et de gérer les accès aux données d'un système d'information. De nombreux modèles de contrôle d'accès existent aujourd'hui, et nous avons introduit un cadre uniforme permettant de définir formellement ces modèles. Ce cadre fournit un guide méthodologique lors de la conception d'un modèle et peut aider un utilisateur à adopter une démarche rigoureuse lors de son développement. De plus, exprimer des modèles au sein d'un même cadre permet de les comparer et d'obtenir une compréhension plus fine des propriétés souhaitées pour le modèle en cours d'élaboration.

L'étude de la comparaison de modèles de contrôle d'accès est un premier pas vers l'étude de la composition de ces modèles. Cette problématique mérite aussi d'être développée puisqu'elle correspond à un problème concret très répandu dans les systèmes d'information. En effet, dans la plupart de ces systèmes, un sujet accède généralement à un objet en passant au travers de plusieurs filtres (par exemple un employé accède aux données du système d'information de son entreprise régi par une certaine politique, après avoir pénétré dans les locaux de cette entreprise, eux-mêmes régis par une autre politique de contrôle
d'accès). Il existe évidemment plusieurs procédés pour composer des politiques de sécurité mais il y a peu d'études sur les propriétés de ces compositions. Nous souhaitons donc étudier cette problématique afin de formaliser les concepts liés à la composition pour pouvoir exprimer les propriétés de sécurité que les mécanismes de composition envisagés peuvent garantir.

La démarche que nous avons adoptée pour aborder la problématique du contrôle d'accès a consisté à étudier plusieurs modèles afin d'en dégager les traits communs et de concevoir un cadre uniforme permettant non seulement de factoriser une partie du travail de développement lors de la conception d'un modèle, mais aussi d'établir des propriétés génériques sur les modèles de contrôle d'accès. Cette démarche peut être appliquée dans d'autres contextes. En collaboration avec V.Delebarre de la société SAFERIVER, j'encadre actuellement le travail de thèse de Liën Tran (débuté en Février 2008) sur la formalisation des propriétés relatives à l'intégrité d'exécution de composants de sécurité. Il s'agit ici non pas de s'assurer que la fonction d'un composant est assurée mais que ce composant fonctionne dans des conditions qui permettent d'avoir confiance dans les résultats qu'il produit. Plus précisément, nous tentons de formaliser les notions d'environnement et d'interfaces d'un composant ainsi que les propriétés que doit respecter ce composant lors de son exécution vis à vis de son environnement et de ses interfaces. Le composant à partir duquel nous travaillons est un composant cryptographique (assurant essentiellement des fonctions de chiffrement et de déchiffrement) dont le fonctionnement est régi par la norme FIPS140-3. Cette norme spécifie les diverses procédures d'initialisation et de chargement des clés ainsi qu'une hiérarchie de modes de fonctionnement du composant, chacun de ces modes garantissant un certain niveau de sécurité.

Les travaux que j'ai présentés sont fortement ancrés sur la logique et la sémantique des langages de programmation. Ces deux paradigmes sont des guides précieux et aussi des garde-fous efficaces pour construire une démarche d'analyse et de construction raisonnée des différents domaines, notions et outils constituant les centres d'interêt de la science informatique. Ils ne sont peut-être pas suffisamment connus ni reconnus. Ces travaux et les activités d'enseignement exercées conjointement peuvent aussi être lus comme une tentative de mieux faire connaître et apprécier ces paradigmes.
Bibliographie

[1] Ocaml-mysql v. 1.0.4 : http://raevnos.pennmush.org/code/ocaml-mysql/.

[2] M.A. Nait Abdallah. On the interpretation of infinite computations in logic programming. In J. Paredaens, editor, *11th International Colloquium on Automata, Languages and Programming, ICALP'84*, volume 172 of *Lecture Notes in Computer Science*, pages 358-370. Springer-Verlag, 1984.

[3] M.A. Nait Abdallah and M.H. van Emden. Top-down semantics of fair computations of logic programs. *Journal of Logic Programming*, 2(1):67-76, 1985.

[4] P. Amey. Dear sir, yours faithfully : an everyday story of formality. In *Practical Elements of Safety, Proc. of the Twelfth Safety-critical Systems Symposium*. Spinger-Verlag, 2004.

[5] J. P. Anderson. Computer Security Technology Planning Study. Technical Report ESD-TR-73-51, USAF Electronic Systems Division, Hanscom Air Force Base, Bedford, Massachusetts, October 1972.

[6] F. Anseaume, J. Baron, P. Berthelin, M. Jacquel, and D. Pipon. Formalisation, spécification et implantation de politiques de contrôle d'accès avec l'atelier focal. Master's thesis, UPMC, Paris, France, 2008.

[7] K.R. Apt. Logic programming. In J. van Leewen, editor, *Handbook of Theoretical Computer Science*, volume B : Formal Models and Semantics, chapter 10, pages 493-574. The MIT Press, New York, 1990.

[8] K.R. Apt and M.H. Van Emden. Contributions to the theory of logic programming. *Journal of the ACM*, 29(3):841-862, 1982.

[9] S. Ayed, N. Cuppens-Boulahia, and F. Cuppens. An integrated model for access control and information flow requirements. In I. Cervesato, editor, *ASIAN*, volume 4846 of *Lecture Notes in Computer Science*, pages 111-125. Springer, 2007.

[10] L. Badger, D.F. Sterne, D.L. Sherman, K.M. Walker, and S.A. Haghighat. Practical domain and type enforcement for UNIX. In *Proceedings of the IEEE Symposium on Research in Security and Privacy*, pages 66-77, Oakland, CA, May 1995. IEEE Computer Society, Technical Committee on Security and Privacy, IEEE Computer Society Press.

[11] G. Barthe and O. Pons. Type isomorphisms and proof reuse in dependent type theory. In F. Honsell and M. Miculan, editors, *Proc. of 4th Int. Conf. on Found. of Software Science and Computation Structures, FoSSaCS'01*, volume 2030 of *Lecture Notes in Computer Science*, pages 57-71. Springer-Verlag, 2001.
[12] D. Bell and L. LaPadula. Secure Computer Systems : a Mathematical Model. Technical Report MTR-2547 (Vol. II), MITRE Corp., Bedford, MA, May 1973.

[13] E. Bertino and R.S. Sandhu. Database security-concepts, approaches, and challenges. *IEEE Trans. Dependable Sec. Comput*, 2(1), 2005.

[14] J. Blond and C. Morisset. Formalisation et implantation d'une politique de sécurité d'une base de données. In INRIA, editor, *17ème Journées Francophones des Langages Applicatifs, JFLA'2006*, pages 71-86, 2006.

[15] J. Blond and C. Morisset. Un moniteur de référence sûr d'une base de données. *Technique et Science Informatiques*, 26(9):1091-1110, 2007.

[16] O. Boite. Proof reuse with extended inductive types. In K.Slind, A.Bunker, and G.Gopalakrishnan, editors, *TPHOLs*, volume 3223 of *Lecture Notes in Computer Science*, pages 50-65. Springer, 2004.

[17] S. Boulmé. *Spécification d'un environnement dédié à la programmation certifiée de bibliothèques de Calcul Formel*. PhD thesis, Université Paris 6, 2000.

[18] F. Brecht and A.D. Kadja. Implantation d'une politique de contrôle d'accès discrétionnaire avec focal. Master's thesis, UPMC, Paris, France, 2007.

[19] D. F. C. Brewer and M. J. Nash. The Chinese Wall Security Policy. In *Proc. IEEE Symposium on Security and Privacy*, pages 206-214, 1989.

[20] M. Carlier and C. Dubois. Functional testing in the Focal environment. In B.Beckert and R.Hähnle, editors, *Tests and Proofs, Second International Conference, TAP 2008, Prato, Italy, April 9-11, 2008. Proceedings*, volume 4966 of *Lecture Notes in Computer Science*, pages 84-98. Springer, 2008.

[21] Pierre Castéran. *An exercice on groups*, 1997. http://coq.inria.fr/contribs/groups.tar.gz.

[22] CC. *Common Criteria for Information Technology Security Evaluation, v3.1*, 2006. http://www.commoncriteriaportal.org/.

[23] A. Chander, J.C. Mitchell, and D. Dean. A state-transition model of trust management and access control. In *Proc. of the 14th IEEE Computer Security Foundations Workshop CSFW*, pages 27-43. IEEE Computer Society Press, 2001.

[24] E. Cohen, R. K. Thomas, W. Winsborough, and D. Shands. Models for coalition-based access control (CBAC). In *SACMAT '02 : Proceedings of the seventh ACM symposium on Access control models and technologies*, pages 97-106. ACM Press, 2002.

[25] A. Colmerauer, H. Kanoui, and M. Van Caneghem. PROLOG, bases théoriques et développements actuels. *Technique et Science Informatiques*, 2(4), 1983.

[26] T. Coquand. Infinite objects in type theory. In H. Barendregt and T. Nipkow, editors, *1st International Workshop on Types for Proofs and Programs, TYPES'93*, volume 806 of LNCS, pages 62-78. Springer-Verlag, 1994.

[27] D. J. Howe. Importing mathematics from HOL into niprl. In J. Von Wright, J. Grundy, and J. Harrison, editors, *Ninth International Conference on Theorem Proving in Higher Order Logics TPHOLs'96*, volume 1125 of *Lecture Notes in Computer Science*, pages 267-282. Springer Verlag, 1996.
[28] A. Santana de Oliveira. *Réécriture et Modularité pour les Politiques de Sécurité*. Phd thesis, Université Henri Poincaré, 2008.

[29] D. Delahaye, J.F. Étienne, and V. Donzeau-Gouge. Certifying airport security regulations using the Focal environment. In J. Misra, T. Nipkow, and E. Sekerinski, editors, *FM 2006 : Formal Methods, 14th International Symposium on Formal Methods, 2006, Proceedings*, volume 4085 of *Lecture Notes in Computer Science*, pages 48–63. Springer, 2006.

[30] D. Delahaye, M. Jaume, and V. Prevosto. Coq : un outil pour l’enseignement. *Technique et Science Informatiques*, 24(9) :1139–1160, 2005.

[31] E. Denney. A prototype proof translator from HOL to Coq. In M. Aagaard and J. Harrison, editors, *13th International Conference on Theorem Proving in Higher Order Logics TPHOLs’2000*, volume 1869 of *Lecture Notes in Computer Science*, pages 108–125. Springer-Verlag, 2000.

[32] D. E. Denning. A lattice model of information flow. *Communications of the ACM*, 19(5) :236–243, May 1976.

[33] D. E. Denning. On the derivation of lattice structured information flow policies. Technical Report TR-179, Dep. of Computer Science, Purdue U., W. Lafayette, Ind., 1976.

[34] D.E. Denning and P.J. Denning. Certification of programs for secure information flow. *Commun. ACM*, 20(7) :504–513, 1977.

[35] P. Deransart and J. Maluszynski. *A Grammatical View of Logic Programming*. The MIT Press, 1993.

[36] C. Dubois and V. Viguié Donzeau-Gouge. A step towards the mechanization of partial functions : domains as inductive predicates. In *Workshop on mechanization of partial functions, CADE 15*, July 1998.

[37] C. Dubois, J. Grandguillot, and M. Jaume. Réutilisation de preuves formelles : Une étude pour le système FoC. In INRIA, editor, *14ème Journées Francophones des Langages Applicatifs, JFLA’2003*, pages 63–75, 2003.

[38] C. Dubois, T. Hardin, and V. Viguié Donzeau Gouge. Building certified components within focal. In *Symposium on Trends in Functional Programming*, 2004.

[39] E. Eder. Properties of substitutions and unifications. *Journal of Symbolic Computation*, 1(1) :31–46, 1985.

[40] A. Felty and D. Howe. Generalization and reuse of tactic proofs. In *Fifth International Conference on Logic Programming and Automated Reasoning, LPAR’94*, volume 822 of *Lecture Notes in Computer Science*, pages 1–15. Springer Verlag, 1994.

[41] A. Felty and D. Howe. Hybrid interactive theorem proving using Nuprl in HOL. In W. McCune, editor, *14th International Conference on Automated Deduction, CADE’14*, volume 1249 of *LNAI*, pages 351–365. Springer Verlag, 1997.

[42] D. F. Ferraiolo and D. R. Kuhn. Role-based access control. In *Proceedings of the 15th National Computer Security Conference*, 1992.

[43] S.N. Foley. Secure information flow using security groups. In *IEEE Computer Security Foundations Workshop CSFW*, pages 62–72, 1990.
[44] J.A. Goguen and R.M. Burstall. Introducing Institutions. In E. Clarke and D. Kozen, editors, *Logics of Programs : Workshop, Carnegie Mellon University, June 1983*, volume 164 of *Lecture Notes in Computer Science*, pages 221–256. Springer-Verlag, 1984.

[45] W.G. Golson. Toward a declarative semantics for infinite objects in logic programming. *Journal of Logic Programming*, 5(2):151–164, 1988.

[46] M.J.C. Gordon, R. Milner, and C. Wadsworth. *Edinburgh LCF : A mechanised logic of computation*. Springer-Verlag, 1979.

[47] E. Gureghian, Th. Hardin, and M. Jaume. A full formalisation of the Bell and La Padula security model. Research Report 2003-007, SPI-LIP6, University Paris 6, 2003.

[48] L. Habib. Formalisation, comparaison et implantation d'un modèle de contrôle d'acès à base de rôles. Master's thesis, UPMC, Paris, France, 2007.

[49] L. Habib, M. Jaume, and C. Morisset. A formal comparison of the Bell & La Padula and RBAC models. In *Fourth International Conference on Information Assurance and Security (IAS'08)*. To appear, IEEE CS Press, 2008.

[50] T. Hardin, M. Jaume, and C. Morisset. Access control and rewrite systems. In *1st International Workshop on Security and Rewriting Techniques, SecRet'06 (Satellite Workshop to ICALP'2006)*, 2006.

[51] M. Harrison, W. Ruzzo, and J. Ullman. Protection in operating systems. *Communications of the ACM*, 19(8):461–471, 1976.

[52] J. Hein. Completions of perpetual logic programs. *Theoretical Computer Science*, 99(1):65–78, 1992.

[53] J. Herbrand. Recherches sur la théorie de la Démonstration (thesis 1930). *Logical Writings*, 1971.

[54] G. Hiet, L. Mé, B. Morin, and V. Viet Triem Tong. Monitoring both OS and program level information flows to detect intrusions against network servers. In *IEEE Workshop on "Monitoring, Attack Detection and Mitigation"*, 2007.

[55] G. Hiet, L. Mé, J. Zimmermann, C. Bidan, B. Morin, and V. Viet Triem Tong. Détection fiable et pertinente de flux d'informations illégaux. In *Proc of the 2nd Conference on Security in Network Architectures and Information Systems (SARSSI)*, 2007.

[56] D. J. Howe. Semantics foundations for embedding HOL in Nuprl. In M. Wirsing and M. Nivat, editors, *Proceedings of the Algebraic Methodology and Software Technology Conference AMAST'96*, volume 1101 of *Lecture Notes in Computer Science*, pages 85–101. Springer-Verlag, 1996.

[57] G. Huet. *A Uniform Approach to Type Theory*, volume Logical Foundations of Functional Programming, pages 337–398. Addison-Wesley, 1990.

[58] J. Jaffar and P.J. Stuckey. Semantics of infinite tree logic programming. *Theoretical Computer Science*, 46(2-3):141–158, 1986.

[59] M. Jaume. Formalisation de la SLD-résolution dans le Calcul des Constructions Inductives. In *Actes des 6èmes Journées Francophones de Programmation Logique et programmation par Contraintes, JFPLC'97*, pages 277–291. Hermès, 1997.
[60] M. Jaume. Unification : a Case Study in Transposition of Formal Properties. In E.L. Gunter and A. Felty, editors, *Supplementary Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics : Poster session TPHOLs'97*, pages 79-93, 1997.

[61] M. Jaume. A full formalisation of SLD-resolution in the Calculus of Inductive Constructions. *Journal of Automated Reasoning*, 23(3-4):347-371, 1999.

[62] M. Jaume. Logic programming and co-inductive definitions. In *Fixed Points in Computer Science, FICS'00 (Workshop to LC'2000)*, 2000.

[63] M. Jaume. Logic programming and co-inductive definitions. In P. Clote and H. Schwichtenberg, editors, *14th International Workshop, CSL'2000, Annual Conference of the European Association for Computer Science Logic*, volume 1862 of *Lecture Notes in Computer Science*, pages 343-355. Springer Verlag, 2000.

[64] M. Jaume. Preuves infinies en programmation logique. In *Actes des 9èmes Journées Francophones de Programmation Logique et programmation par Contraintes, JFPLC'2000*, pages 33-47. Hermès, 2000.

[65] M. Jaume. On greatest fixpoint semantics of logic programming. *Journal of Logic and Computation*, 12(2):321-342, 2002.

[66] M. Jaume and C. Dubois. Formalisation of general logics in the Calculus of Inductive Constructions : Towards an abstract development to assist formal specification of logics. Research Report 37-1999, LaMI, University of Evry, France, 1999.

[67] M. Jaume and C. Morisset. Formalisation and implementation of access control models. In *Information Assurance and Security (IAS'05) International Conference on Information Technology, ITCC*, pages 703-708. IEEE CS Press, 2005.

[68] M. Jaume and C. Morisset. A formal approach to implement access control. *Journal of Information Assurance and Security*, 2:137-148, June 2006.

[69] M. Jaume and C. Morisset. Towards a formal specification of access control. In *Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis FCS-ARSPA'06 (Workshop to LICS'2006)*, 2006.

[70] M. Jaume and C. Morisset. Contrôler le contrôle d'accès : Approches formelles. In *Approches Formelles dans l'Assistance au Développement de Logiciels, AFADL'07*, 2007.

[71] M. Jaume and C. Morisset. Un cadre sémantique pour le contrôle d'accès. *Technique et Science Informatiques*, 2008.

[72] A. Abou El Kalam, R. El Baida, P. Balbiani, S. Benferhat, F. Cuppens, Y. Deswarte, A. Miège, C. Saurel, and G. Trouessin. Organization based access control. In *Policy'2003*, Como, Italie, June 2003.

[73] A. Abou El Kalam, S. Benferhat, A. Miège, R. El Baida, F. Cuppens, C. Saurel, P. Balbiani, Y. Deswarte, and G. Trouessin. Organization based access control. In *IEEE 4th International Workshop on policies for distributed systems and networks*, page 120. IEEE Computer Society, 2003.

[74] R.S. Kemp and G.A. Ringwood. Reynolds and Heyting models of logic programs. In *ICLP94 Workshop on Proof Theoretical extensions of logic programming*, 1994.
[75] C. Kirchner and H. Kirchner. Rewriting, solving, proving, 2006.

[76] H.P. Ko and M.E. Nadel. Substitution and refutation revisited. In Koichi Furukawa, editor, *Proceedings of the Eighth International Conference on Logic Programming*, pages 679–692. The MIT Press, 1991.

[77] T. Kolbe and C. Walther. Proof analysis, generalization, and reuse. In W. Bibel and P. H. Schmidt, editors, *Automated Deduction : A Basis for Applications. Volume II, Systems and Implementation Techniques*. Kluwer Academic Publishers, 1998.

[78] R. Lalement. *Computation as Logic*. Prentice Hall International Series in Computer Science, 1993.

[79] B.W. Lampson. Protection. *Operating Systems Review*, 8(1):18–24, January 1974.

[80] L.J. LaPadula and D.E. Bell. Secure Computer Systems : A Mathematical Model. *Journal of Computer Security*, 4:239–263, 1996.

[81] J.L. Lassez, M. Maher, and K. Mariott. Unification revisited. In J. Minker, editor, *Foundations of Deductive Databases and Logic Programming*, pages 587–625. M. Kaufman, Los Altos, California, 1987.

[82] J.L. Lassez and M.J. Maher. Closures and fairness in the semantics of programming logic. *Theoretical Computer Science*, 29(1-2):167–184, 1984.

[83] H.M. Levy. *Capability-Based Computer Systems*. Digital Press, Bedford, MA, 1984.

[84] J.W. Lloyd. *Foundations of Logic Programming*. Springer-Verlag, second, extended edition, 1987.

[85] J.W. Lloyd and J.C. Sheperdson. Partial evaluation in logic programming. *Journal of Logic Programming*, 11(3-4):217–242, 1991.

[86] N. Magaud and Y. Bertot. Changing data structures in type theory : a study of natural numbers. In P. Callaghan, Z. Luo, J. McKinna, and R. Pollack, editors, *Types for Proofs and Programs TYPES’2000*, volume 2277 of *Lecture Notes in Computer Science*, pages 181–196. Springer-Verlag, 2000.

[87] Z. Manna and R.J. Waldinger. Deductive synthesis of the unification algorithm. *Science of Computer Programming*, 1(1-2):5–48, 1981.

[88] Z. Manna and R.J. Waldinger. Fundamentals of deductive program synthesis. *IEEE Transactions on Software Engineering*, 18(8):674–704, 1992.

[89] McLean. The algebra of security. In *Proc. IEEE Symposium on Security and Privacy*, pages 2–7. IEEE Computer Society Press, 1988.

[90] J. McLean. Security models and information flow. In *Proceedings of the IEEE Symposium on Research in Security and Privacy*, pages 180–187, 1990.

[91] J Meseguer. General logics. In H.-D. Ebbinghaus et al., editors, *Logic Colloquium '87*. North-Holland Publishing Co., 1989.

[92] A. Mikhajlova and J. Von Wright. Proving isomorphism of first-order logic proof systems in HOL. In J. Grundy and M. Newey, editors, *11th International Conference on Theorem Proving in Higher Order Logics TPHOLs'98*, volume 1479 of *Lecture Notes in Computer Science*, pages 295–314. Springer Verlag, 1998.

[93] C. Morisset. *Sémantique des systèmes de contrôle d'accès*. PhD thesis, Université Pierre et Marie Curie, 2007.
[94] C. Morisset and A. Santana de Oliveira. Automated detection of information leakage in access control. In *Proceedings of the 2nd International Workshop on Security and Rewriting Techniques (SecReT'07)*, Paris, France, 2007.

[95] P. Naumov. Formalization of isabelle meta logic in nuPRL. Technical Report TR99-1769, Cornell University, Computer Science, 1999.

[96] P. Naumov. Importing isabelle formal mathematics into nuPRL. Technical Report TR99-1734, Cornell University, Computer Science, 1999.

[97] N.J. Nilsson. *Principles of Artificial Intelligence*. Symbolic Computation. Springer-Verlag, 1982.

[98] U. Nilsson and J. Maluszynski. *Logic Programming and Prolog*. Wiley, 1990.

[99] S.L. Osborn. Information flow analysis of an RBAC system. In *7th ACM Symposium on Access Control Models and Technologies SACMAT*, pages 163–168, 2002.

[100] C. Palamidessi. Algebraic properties of idempotent substitutions. In M.S. Paterson, editor, *Proceedings, 17th International Colloquium on Automata, Languages and Programming (ICALP)*, volume 443 of *Lecture Notes in Computer Science*, pages 386–399. Springer-Verlag, 1990.

[101] C. Paulin-Mohring. Inductive definitions in the system COQ. Rules and properties. In M. Bezem and J.F. Groote, editors, *Proceedings of the 1st International Conference on Typed Lambda Calculi and Applications, TCLA'93*, volume 664 of *Lecture Notes in Computer Science*, pages 328–345. Springer-Verlag, 1993.

[102] L.C. Paulson. Verifying the unification algorithm in LCF. *Science of Computer Programming*, 5:143–169, 1985.

[103] L.C. Paulson and A.W. Smith. Logic programming, functional programming, and inductive definitions. In P. Schroeder-Heister, editor, *International Workshop on Extensions of Logic Programming*, volume 475 of LNCS, pages 283–310. Springer-Verlag, 1989.

[104] A. Podelski, W. Charatonik, and M. Müller. Set-based failure analysis for logic programs and concurrent constraint programs. In S. Doaitse Swierstra, editor, *8th European Symposium on Programming, ESOP'99*, LNCS, pages 177–192. Springer-Verlag, 1999.

[105] O. Pons. Ingénierie de la preuve. In INRIA, editor, *Onzièmes Journées Francophones des Langages Applicatifs, JFLA'2000*, 2000.

[106] V. Prevosto. *Conception et Implantation du langage FoC pour le développement de logiciels certifiés*. PhD thesis, Université Paris 6, sep 2003.

[107] V. Prevosto and D. Doligez. Algorithms and proof inheritance in the Foc language. *Journal of Automated Reasoning*, 29(3-4):337–363, dec 2002.

[108] V. Prevosto, D. Doligez, and Th. Hardin. Algebraic structures and dependent records. In C. Munoz, S. Tahar, and V. Carreno, editors, *TPHOLs : 15th International Workshop on Higher Order Logic Theorem Proving and Its Applications*, volume 2410. LNCS, Springer-Verlag, aou 2002.

[109] V. Prevosto and M. Jaume. Making proofs in a hierarchy of mathematical structures. In *11th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2003*, pages 89–100. Aracne, 2003.
[110] Focal project. *Focal, version 0.2 Tutorial and reference manual.* LIP6 – INRIA – CNAM, sept 2004. Distribution available at : http://focal.inria.fr.

[111] C. Renard. *Un peu d'extensionnalité en Coq - une tactique pour les sétoïdes*. Mémoire de DEA, Université Paris 7, 2001.

[112] R. Rioboo. *Programmer le Calcul Formel, des Algorithmes à la Sémantique, Mémoire d'Habilitation*. Mémoire d'habilitation, Université Pierre et Marie Curie, Paris, France, 2002.

[113] A.J. Robinson. A machine-oriented logic based on the resolution principle. *Journal of the ACM*, 12(1), 1965.

[114] A.J. Robinson. *Logic : Form and Function. The Mechanization of Deductive Reasoning*. Edinburgh University Press, 1979.

[115] J. Rouyer. Développement de l’algorithme d’unification dans le Calcul des Constructions avec Types Inductifs. Research Report 1795, INRIA-Lorraine, 1992.

[116] Sandhu and Chen. The multilevel relational (MLR) data model. *ACMTISS : ACM Transactions on Information and System Security*, 1, 1998.

[117] R. S. Sandhu, E. J. Coyne, H. L. Feinstein, and C. E. Youman. Role-based access control models. *IEEE Computer*, 29(2):38–47, 1996.

[118] E.Y. Shapiro. Alternation and the computational complexity of logic programs. *Journal of Logic Programming*, 1(1):19–33, 1984.

[119] J.C. Shepherdson. The role of standardising apart in logic programming. *Theoretical Computer Science*, 129(1):143–166, 1994.

[120] L. Sterling and E. Shapiro. *The Art of Prolog : Advanced Programming Techniques*. MIT Press, Cambridge, Ma, 1986.

[121] R. K. Thomas. Team-based access control (tmac) : a primitive for applying role-based access controls in collaborative environments. In *RBAC '97 : Proceedings of the second ACM workshop on Role-based access control*, pages 13–19. ACM Press, 1997.

[122] M.V. Tripunitara and N. Li. Comparing the expressive power of access control models. In *11th ACM Conf. on Computer and Communications Security*. ACM SIGSAC, 2004.

[123] M.C. Tschantz and S. Krishnamurthi. Towards reasonability properties for access-control policy languages. In D.F. Ferraiolo and I. Ray, editors, *Proceedings of SAC-MAT 2006*, pages 160–169. ACM, 2006.

[124] M.H. van Emden and R.A. Kowalski. The semantics of predicate logic as a programming language. *Journal of the ACM*, 23(4):733–742, 1976.
# Annexe A

## L'atelier Focal

L'atelier Focal [110, 38, 107], et la méthodologie sous-jacente, ont initialement été conçus pour répondre au besoin d'accroître la confiance dans les résultats fournis par les algorithmes de calcul formel. C'est en fait ce domaine qui a servi de modèle et donné les lignes directrices du développement de l'atelier. Grâce à l'atelier Focal, R. Rioboo a pu construire une bibliothèque de calcul formel conséquente [112] comprenant des algorithmes complexes et dont l'efficacité est comparable à celle des meilleurs systèmes de calcul formel. Focal est maintenant utilisé dans différents domaines et en particulier dans le domaine de la sécurité. Outre les développements que nous effectuons avec Focal sur les politiques de contrôle d'accès, Focal a été utilisé avec succès pour formaliser la politique de sécurité au sol d'un aéroport [29].

L'atelier Focal [106, 107, 108, 38, 110] fournit un environnement de développement intégré (IDE) logiquement fondé, avec une sémantique claire et qui permet d'obtenir des implantations efficaces. Focal offre un langage muni de traits objets (héritage multiple, liaison tardive, redéfinition, ...) permettant non seulement de structurer un développement de manière à le rendre facilement réutilisable, mais aussi d'obtenir un logiciel par raffinements successifs en passant progressivement de la spécification à l'implantation. Focal permet d'écrire au sein d'un même cadre de travail des spécifications, des programmes et des preuves. Cet atelier permet aux programmeurs d'écrire des preuves formelles de leur code. Ils sont aidés dans leur tâche par Zenon, un démonstrateur automatique. Les preuves obtenues sont vérifiées par Coq.

Un programme Focal est la donnée d'une hiérarchie d'espèces. Une espèce peut être vue comme un ensemble de méthodes, identifiées par leur nom. Chaque méthode peut être soit déclarée ( constantes, opérations et propriétés ) soit définie ( implantations des opérations et preuves des théorèmes ), et appartient à l'une des trois classes suivantes :

- Le type support est la méthode qui représente l'ensemble sous-jacent à la structure définie par l'espèce. Chaque espèce doit avoir un seul type support, et il peut être soit déclaré soit défini. Un type support seulement déclaré correspond alors à un type abstrait de données, et un type support défini correspond à un type concret.

- Les méthodes opérationnelles sont les constantes ou les fonctions de la structure. Les méthodes qui ne sont que déclarées sont appelées des signatures. Le langage utilisé pour définir ces méthodes est similaire à celui du noyau fonctionnel d'OCaml, avec une construction permettant d'appeller une méthode d'une espèce donnée.
<figure><img src="image_11.png" /><figcaption>FIG. A.1 – Construction d'un programme Focal</figcaption></figure>

- Les méthodes logiques décrivent les propriétés des méthodes opérationnelles. Dans ce contexte, la déclaration d'une méthode logique est simplement l'énoncé d'une propriété, tandis que la définition d'une méthode logique est la preuve que cette propriété est vraie.

Le langage utilisé pour les énoncés de propriétés est composé des connecteurs logiques de base et des quantificateurs existentiels et universels sur les types Focal. Ces propriétés sont donc des formules de logique du premier ordre, contenant les noms des méthodes liées par déclaration/définition, héritage ou paramétrisation.

Au bas de la hiérachie Focal, on trouve les collections. Une collection est construite sur une espèce complétement définie (toutes les méthodes opérationnelles sont définies et toutes les méthodes logiques sont prouvées). De plus, une collection est "figée", dans le sens où on ne peut plus en hériter, et on ne peut pas définir de nouvelles méthodes ni en redéfinir. Enfin, toutes les définitions (type support et preuves compris) sont masquées à l'utilisateur afin que ce dernier n'ait accès qu'à l'interface de la collection (noms des méthodes et propriétés). La figure A.1 illustre la construction d'une hiérarchie d'espèces Focal.

La compilation d'un programme Focal s'effectue en plusieurs étapes. Le fichier source est analysé par le compilateur, qui effectue un calcul de dépendances permettant d'éliminer des cycles dans les dépendances (condition suffisante pour éviter des incohérences logiques [17]), de gérer l'héritage multiple et la liaison tardive (relier un nom de méthode à sa définition la plus récente), d'effacer les preuves dépendant des définitions de fonctions en cas de redéfinition de celles-ci. Puis, le fichier est compilé vers un fichier Ocaml, qui correspond, une fois compilé, à un programme exécutable. Le fichier est également compilé vers un source Coq, contenant toute la structuration du programme ainsi que toutes
les preuves. Chaque preuve écrite en Zenon est analysée par cet outil, et transformée en
un terme de preuve Coq. Enfin, le fichier est compilé vers un format intermédiaire de
documentation, permettant de générer du XML, du LaTeX, de l'UML, etc. Un outil per-
mettant de démontrer la terminaison des fonctions récursives est en cours d'intégration.
Focal propose également un outil de génération automatique de test et un outil graphique
de représentation des dépendances entre espèces et méthodes.
# Annexe B

## Formalisations

### B.1 Unification des termes du premier ordre

#### B.1.1 Formalisation de l'unification dans le système Coq

L'unification est une opération de nature syntaxique permettant de résoudre un système d'équations entre termes du premier ordre. Cette opération est la "cheville ouvrière" de nombreux algorithmes de démonstration automatique et de systèmes d'aide à la preuve. Dans le domaine de la programmation, l'unification joue un rôle central dans certains algorithmes de typage et en programmation logique. Si les algorithmes d'unification de termes du premier ordre sont aujourd'hui bien connus et bien maîtrisés, leur implantation est parfois délicate et source de confusions. En effet, l'unification repose sur la notion de substitution, notion pour laquelle, comme nous le verrons, coexistent plusieurs définitions non-équivalentes. Aussi, j'ai entrepris la mécanisation, avec le système Coq, de la preuve de la décidabilité du problème de l'unification des termes du premier ordre [60]. L'objectif de ce développement est double : tout d'abord, grâce au mécanisme d'extraction du système Coq, j'ai obtenu un programme certifié implantant l'unification ; enfin, le développement obtenu a servi de base à la formalisation de la sémantique de la programmation logique présentée dans la section B.2.

Etant donnés une signature $\Sigma$ (i.e. un ensemble dénombrable muni d'une application $ar : \Sigma \to \mathbb{N}$) et un ensemble dénombrable $X$ de symboles de variables, l'ensemble $T_\Sigma[X]$ des termes est défini de manière inductive :

- Un symbole de variable est un terme.

- Si $f \in \Sigma$ est un symbole d'arité $n > 0$, et si $t_1, \dots, t_n$ sont des termes, alors $f(t_1, \dots, t_n)$ est un terme.

Deux termes $t_1$ et $t_2$ sont dits *unifiables* si il existe une substitution $\theta$ telle que $\theta(t_1) = \theta(t_2)$. Décider si deux termes $t_1$ et $t_2$ sont unifiables revient à résoudre l'équation $t_1 = t_2$. Plus généralement, l'algorithme d'unification permet de résoudre un système d'équations $E$ entre termes en transformant $E$ en un système de la forme $\bigcup_1^n \{x_i = t_i\}$, tel que les variables $x_i$ soient deux à deux distinctes et tel que $\{x_1, \dots, x_n\} \cap \bigcup_1^n \text{var}(t_i) = \emptyset$ ($\text{var}(t)$ dénote l'ensemble des variables apparaissant dans le terme $t$), si $E$ admet une solution (et dans ce cas, ce système correspond à une substitution) ou en un système noté $\{\perp\}$ si $E$ n'admet pas de solution. Un tel système est dit *résolu*. L'algorithme d'unification peut être vu comme la définition d'une relation de transition, notée $\rightsquigarrow$. Résoudre un système d'équations $E$
<table><caption>TAB. B.1 – Algorithme d'unification</caption><tr><td>{f(t<sub>1</sub>, ..., t<sub>n</sub>) = f(t'<sub>1</sub>, ..., t'<sub>n</sub>)} &cup; E</td><td>décomposition</td><td>{t<sub>1</sub> = t'<sub>1</sub>, ..., t<sub>n</sub> = t'<sub>n</sub>} &cup; E</td></tr><tr><td>{f(t<sub>1</sub>, ..., t<sub>n</sub>) = g(t'<sub>1</sub>, ..., t'<sub>n</sub>)} &cup; E</td><td>conflit</td><td>{⊥} si f &ne; g</td></tr><tr><td>{x = t} &cup; E</td><td>élimination</td><td>{x = t} &cup; E[x &leftarrow; t] si x &isin; var(E) et x &notin; var(t)</td></tr><tr><td>{x = t} &cup; E</td><td>occurrence</td><td>{⊥} si x &isin; var(t)</td></tr><tr><td>{t = t} &cup; E</td><td>effacement</td><td>E</td></tr><tr><td>{t = x} &cup; E</td><td>inversion</td><td>{x = t} &cup; E si t &notin; X</td></tr></table>

entre termes revient alors à construire une suite de transitions $E \rightsquigarrow E_1 \rightsquigarrow \dots \rightsquigarrow E_n$ telle que le système $E_n$ soit résolu. Cet algorithme, introduit pour la première fois par J. Herbrand [53], est classique et est rappelé dans le tableau B.1. Le développement que j'ai effectué avec le système Coq est une mécanisation des définitions classiques des termes et des substitutions, et de la preuve de la propriété suivante :

$$ \forall t_1, t_2 \in T_{\Sigma}[X] \ (\exists \theta \ mgu(\theta, t_1, t_2)) \lor (\forall \theta \ \theta(t_1) \neq \theta(t_2)) $$

où $mgu(\theta, t_1, t_2)$ signifie que $\theta$ est une substitution minimale, idempotente, ne portant que sur les variables apparaissant dans les termes $t_1$ et $t_2$ et telle que $\theta(t_1) = \theta(t_2)$. Un programme implantant un algorithme d'unification a été extrait de la preuve obtenue. Ce travail permet donc de disposer d'une implantation certifiée de l'algorithme d'unification, qui peut être utilisée avec profit dans les nombreux domaines où l'unification constitue un mécanisme de base (programmation logique, typage, ...).

## B.1.2 Formaliser ce qui semble déjà formel ?

De nombreux ouvrages et articles décrivent les algorithmes d'unification des termes du premier ordre. Ces algorithmes portent sur des objets à l' "allure mathématique" sur lesquels il est donc possible d'établir des propriétés dans un cadre assez formel. Il peut alors paraître inutile d'utiliser un outil comme Coq pour décrire cette théorie. Toutefois, la notion de substitution n'est pas aussi simple qu'il y paraît et la littérature en fournit de nombreuses présentations différentes. Bien sûr, selon les goûts et les besoins de chacun, plusieurs définitions (et représentations) équivalentes peuvent exister. Cependant, dans le domaine de l'informatique, il est surprenant de constater que plusieurs définitions non équivalentes coexistent : en 1991, H.P. Ko et M.E. Nadel [76] recensaient les définitions suivantes.

- Une substitution est une fonction de X dans $T_{\Sigma}[X]$.

- E. Eder [39], C.Kirchner et H.Kirchner [75] définissent une substitution comme une fonction $\theta$ de X dans $T_{\Sigma}[X]$ pour laquelle l'ensemble $\{x \in X, \theta(x) \neq x\}$ est fini (i.e. $\theta$ est l'identité presque partout).
- E.Y.Shapiro [118] définit une substitution comme une fonction $\theta$ d'un sous-ensemble fini de $X$ dans $T_{\Sigma}[X]$ (i.e. $\theta$ est une fonction partielle).

- K.R.Apt [7], J.L.Lassez, M.Maher et K.Mariott [81] et J.W.Lloyd [84] définissent une substitution comme une fonction $\theta$ d'un sous-ensemble fini $D \subseteq X$ dans $T_{\Sigma}[X]$ telle que pour tout $x \in D$, $\theta(x) \neq x$.

- N.J.Nilsson [97] définit une substitution comme une fonction $\theta$ d'un sous-ensemble fini $D \subseteq X$ dans $T_{\Sigma}[X]$ telle que pour tout $x \in D$, $x \notin \theta(x)$.

- L.Sterling et E.Y.Shapiro [120] définissent une substitution comme une fonction $\theta$ d'un sous-ensemble fini $D \subseteq X$ dans $T_{\Sigma}[X]$ telle que pour tout $x \in D$ et tout $y \in D$, $x \notin \theta(y)$.

Ces définitions ne sont pas toutes équivalentes et H.P. Ko et M.E. Nadel [76] étudient l'influence du choix d'une définition en examinant les propriétés vérifiées par la relation "est une instance de" en fonction de la définition utilisée. Ainsi, selon la définition employée, cette relation peut ne pas être transitive ou même ne pas impliquer l'unifiabilité des deux termes qu'elle relie. Ces constatations sont surprenantes et ne correspondent pas toujours aux propriétés de l'"objet informel" que l'on croit manipuler. Les substitutions sont donc des objets qu'il faut définir formellement et manipuler avec précaution.

Evidemment ces problèmes réapparaissent lors de la définition d'un unificateur et de la caractérisation de ses propriétés lors de la conception d'algorithmes d'unification. En 1987, E. Eder [39] consacre un article entier aux propriétés algébriques des substitutions idempotentes permettant d'envisager l'unification d'ensembles de termes. En 1987, dans le même esprit, J.L. Lassez, M.J. Maher et K. Marriott [81] revisitent l'unification en considérant un treillis de contraintes d'égalité et exhibent les différences qui existent entre les définitions d'un unificateur principal que l'on peut rencontrer dans la littérature. Parmi elles, citons les quatre suivantes :

- A.J.Robinson [113] définit un unificateur principal comme étant la substitution produite par l'algorithme présenté dans [113].

- A.J.Robinson [114] définit un unificateur principal comme une substitution $\theta$ telle que pour tout autre unificateur $\sigma$, $\sigma = \sigma\theta$.

- J.W.Lloyd [84] définit un unificateur principal comme une substitution $\theta$ telle que pour tout autre unificateur $\sigma$, il existe une substitution $\mu$ telle que $\sigma = \mu\theta$.

- L.Sterling et E.Y.Shapiro [120] définissent un unificateur principal relativement à un ordre partiel sur les termes comme étant la substitution qui transforme deux termes en leur instance commune la plus générale.

Comme nous le verrons dans la section B.2, ici encore, le choix d'une définition n'est pas sans conséquence. Certaines erreurs peuvent en effet apparaître lorsque l'on "combine" des résultats sur l'unfication qui ont été établis de manière indépendante et qui reposent sur des définitions non équivalentes.

La formalisation de la preuve du théorème de décidabilité de l'unification des termes du premier ordre permet donc d'expliciter complètement les notions sur lesquelles elle repose. Enfin, j'ai obtenu cette preuve par réutilisation de la preuve de cette propriété sur un ensemble plus large : l'ensemble des quasi-termes. Ce développement a donc aussi permis de dégager une méthodologie de réutilisation de preuves formelles présentée dans la section C.1.1.
## B.2 Sémantique de la programmation logique

Définir formellement la sémantique d'un langage de programmation et établir les propriétés que garantit cette sémantique offre, d'une part à celui qui programme dans ce langage de disposer d'une sémantique claire, précise et non ambiguë, et, d'autre part, à celui qui conçoit un interpréteur ou un compilateur pour ce langage d'en garantir la correction. Cette section présente les formalisations que j'ai effectuées pour étudier la sémantique de la programmation logique.

Issue de la recherche en démonstration automatique en logique du premier ordre, et basée sur le principe de résolution de A.J. Robinson [113], la programmation logique a été introduite dans la pratique par A. Colmerauer (langage PROLOG, 1972) [25] tandis que ses fondements théoriques ont été établis par R.A. Kowalski et M.H. van Emden [124]. Ce paradigme de programmation est né de la découverte d'un sous-ensemble de la logique du premier ordre (aussi appelé le fragment Hornien de la logique des prédicats) associé à une interprétation opérationnelle correcte et complète, basée sur la SLD-résolution (Selection Linear Definite).

Un programme logique est un ensemble fini de clauses, notées $A \leftarrow B_1, \dots, B_n$ où $A$ et $B_i$ ($1 \le i \le n$) désignent des atomes (de la forme $p(t_1, \dots, t_k)$ où $p$ est un symbole de prédicat et $t_1, \dots, t_n$ sont des termes). Plusieurs lectures d'un programme logique sont possibles, donnant lieu à différentes sémantiques. Traditionnellement, on distingue la sémantique déclarative d'un programme de sa sémantique opérationnelle. D'un point de vue déclaratif, la clause $A \leftarrow B_1, \dots, B_n$ peut s'interpréter par “si $B_1$ et $\dots$ et $B_n$ sont vrais, alors $A$ est vrai”. Dans ce cas, une clause spécifie une relation logique entre formules atomiques exprimée par la formule quantifiée universellement $\forall \vec{x}(A \lor \neg B_1 \lor \dots \lor \neg B_n)$ (ou de manière logiquement équivalente par $\forall \vec{x}(B_1 \land \dots \land B_n \Rightarrow A)$). Une clause négative (aussi appelée but) est une clause de la forme $\leftarrow B_1, \dots, B_q$ dont la signification logique est donnée par la formule $\forall \vec{x}(\neg B_1 \lor \dots \lor \neg B_q)$ (ou de manière logiquement équivalente par $\neg \exists \vec{x}(B_1 \land \dots \land B_q)$). L'exécution d'un programme $P$ à partir d'un but $\leftarrow B_1, \dots, B_q$ consiste à réfuter l'ensemble $P \cup \{\forall \vec{x}(\neg B_1 \lor \dots \lor \neg B_q)\}$, ce qui revient, d'un point de vue déclaratif, à prouver à partir de $P$, la formule existentielle $\exists \vec{x}(B_1 \land \dots \land B_q)$, appelée requête. Cette preuve est obtenue de manière constructive : un résultat est extrait de la preuve de $\exists \vec{x}(B_1 \land \dots \land B_q)$ et correspond à une affectation des variables de $\vec{x}$. Il s'agit d'une substitution $\theta$, appelée solution, telle que $P \models \forall \vec{z} \theta(B_1 \land \dots \land B_q)$ où $\models$ dénote la relation de conséquence sémantique. Cette lecture logique des programmes ne fournit aucune information quant à la manière dont le programme, en tant que processus de preuve, s'exécute.

D'un point de vue opérationnel, la clause $A \leftarrow B_1, \dots, B_n$ peut se comprendre comme une procédure $A$ dont l'appel engendrerait l'exécution des $B_i$. Cette interprétation opérationnelle des programmes est définie par la SLD-résolution. Cette règle permet de déduire une clause à partir d'une clause et d'un but :

$$ (\text{SLD-résolution}) \quad \frac{A \leftarrow A_1, \dots, A_n \quad \leftarrow B_1, \dots, B_q}{\leftarrow \theta(B_1, \dots, B_{i-1}, A_1, \dots, A_n, B_{i+1}, \dots, B_q)} $$

où $\theta$ est un unificateur principal du $i$-ième atome $B_i$ ($1 \le i \le q$) du but et de $A$. Cette
règle peut être vue comme une relation de transition notée :

$$ \leftarrow B_1, \dots, B_q \quad \xrightarrow{C, \theta} \quad \leftarrow \theta(B_1, \dots, B_{i-1}, A_1, \dots, A_n, B_{i+1}, \dots, B_q) $$

où C est la clause $A \leftarrow A_1, \dots, A_n$. C est donc utilisée avec le but $\leftarrow B_1, \dots, B_q$ pour déduire $\theta(B_1, \dots, B_{i-1}, A_1, \dots, A_n, B_{i+1}, \dots, B_q)$ à partir de la règle de SLD-résolution avec l'unificateur principal $\theta$. L'exécution d'un programme logique P à partir d'un but $R_0$ est décrite par une dérivation, définie comme une succession de transitions :

$$ R_0 \xrightarrow{C_0, \theta_0} R_1 \xrightarrow{C_1, \theta_1} \dots R_{i-1} \xrightarrow{C_{i-1}, \theta_{i-1}} R_i \xrightarrow{C_i, \theta_i} \dots $$

où $C_0, C_1, \dots$ sont des variantes de clauses de P (i.e. des clauses de P renommées). La substitution construite par cette dérivation, appelée réponse, est la composition des substitutions calculées à chaque étape. Un aspect fondamental de la programmation logique est la correspondance complète entre ces deux lectures sémantiques. Cette correspondance se révèle aussi utile d'un point de vue plus pratique : elle permet de comprendre le résultat de l'exécution d'un programme logique à partir d'une requête sans en connaître nécessairement le mécanisme d'exécution. Signalons ici qu'il existe bien d'autres lectures de la programmation logique : réécriture, résolution d'équations, preuve de théorème, réseau de processus communicants ... D'autre part, de nombreuses extensions ont été proposées afin d'augmenter la puissance d'expression de ce modèle de programmation : négation, contraintes, concurrence, ordre supérieur ...

## B.2.1 Plongement profond : Formaliser pour corriger

### Substitutions et unificateurs

La sémantique de la programmation logique s'exprime à l'aide d'objets "bien connus" : substitutions, unificateurs, conditions de renommage. S'agissant d'objets à l' "allure mathématique", ici encore, on peut s'interroger sur l'utilité de la formalisation de la théorie de la programmation logique. Toutefois, le rôle central que joue la notion de substitution dans cette théorie et l'existence de plusieurs définitions non équivalentes pour cette notion et celle d'unificateur principal a bien entendu des répercussions dans le domaine de la programmation logique. Par exemple, le recensement des différentes définitions des substitutions a permis à H.P. Ko et M.E. Nadel [76] de corriger certaines erreurs dans la preuve du lemme de généralisation présentée dans [84]. D'ailleurs, afin d'éviter les problèmes liés à l'utilisation des substitutions lors de la définition de la sémantique des programmes logiques, R.S. Kemp et G.A. Ringwood [74] préfèrent baser directement cette sémantique sur la relation "est une instance de". Dans le même esprit, C. Palamidessi [100] définit une algèbre des substitutions idempotentes, proche de celle proposée par E. Eder dans [39], munie d'opérateurs satisfaisant de "bonnes" propriétés permettant d'envisager la définition d'une sémantique déclarative compositionnelle et la parallélisation du processus d'exécution des programmes logiques.

Le développement que j'ai effectué relève donc d'une démarche minutieuse dont l'objectif est de détailler tous les mécanismes des preuves de la théorie classique de la programmation logique en mettant en évidence le rôle crucial qu'occupent certains détails généralement ignorés. Cette formalisation correspond donc à un souci de corriger et/ou de
préciser des résultats standards incorrectement formulés et/ou prouvés. Un des exemples les plus célèbres d'énoncé inexact concerne une propriété fondamentale de la programmation logique. Il s'agit du théorème de compléture de la SLD-résolution, énoncé par J.W. Lloyd [84], dans un ouvrage qui fait référence en la matière, sous la forme suivante :

(Completeness [84]) Let P be a definite program and G a definite goal. For every correct answer $\theta$ for $P \cup \{G\}$, there exists a computed answer $\sigma$ for $P \cup \{G\}$ and a substitution $\gamma$ such that $\theta = \gamma\sigma$.

où la notion de réponse correcte correspond à celle de solution, introduite précédemment. En 1994, J.C. Shepherdson invalide cet énoncé [119] et présente le contre-exemple suivant. Si $G$ est le but $\leftarrow p(x)$ et $P$ le programme contenant l'unique clause $p(f(y, z)) \leftarrow$, alors pour une constante $a$ du langage, la substitution<fnref n="1" /> $\theta = \{x/f(a, a)\}$ est solution. Les variantes de la clause de $P$, de la forme $p(f(x_1, x_2)) \leftarrow$, s'unifient avec $G$ via l'unificateur le plus général $\{x/f(x_1, x_2)\}$ (lorsque $x_1 \neq x$ et $x_2 \neq x$). Aussi, la réponse calculée par une dérivation à partir de $G$ est de la forme $\sigma = \{x/f(x_1, x_2)\}$. Toutefois, il n'existe pas de substitution $\gamma$ telle que $\theta = \gamma\sigma$. En effet, les variables $x_1$ et $x_2$ devraient appartenir au domaine d'une telle substitution, alors qu'elles n'appartiennent pas au domaine de la substitution $\theta$. Pour obtenir un énoncé correct, il suffit donc de remplacer la conclusion $\theta = \gamma\sigma$ par $\theta G = \gamma\sigma G$.

## Explicitation du renommage

Ce développement a mis en relief le rôle crucial des mécanismes de renommage, souvent implicites dans la littérature, et sources d'erreurs. Comme pour les définitions des substitutions ou des unificateurs principaux, plusieurs définitions des conditions de renommage des variables des clauses mises en jeu lors de l'exécution des programmes logiques coexistent dans la littérature. Différentes conditions de renommage des clauses lors d'une dérivation :

$$R_0 \xrightarrow{C_0, \theta_0} R_1 \xrightarrow{C_1, \theta_1} \dots R_{i-1} \xrightarrow{C_{i-1}, \theta_{i-1}} R_i \xrightarrow{C_i, \theta_i} \dots$$

apparaissent dans la littérature :

- K.R.Apt et M.H.Van Emden [8], R.Lalement [78] et J.L.Lassez et M.J.Maher [82] imposent que chaque clause $C_i$ ne partage pas de variables avec $R_i : var(C_i) \cap var(R_i) = \emptyset$.

- J.W.Lloyd [84] impose que chaque clause $C_i$ ne contienne pas de variables apparaisant déjà dans la dérivation jusqu'à $R_i$.

- U.Nilsson et J.Maluszynski [98] imposent que chaque clause $C_i$ ne partage pas de variables avec $R_i$ et $R_0 : var(C_i) \cap (var(R_0) \cup var(R_i)) = \emptyset$.

- K.R.Apt [7] impose que chaque clause $C_i$ ne partage aucune variable avec $R_0$, $C_0$, $C_1$, ..., $C_{i-1} : var(C_i) \cap (var(R_0) \cup var(C_0) \cup \dots \cup var(C_{i-1})) = \emptyset$.

Considérons par exemple le programme $P = \{p(f(x)) \leftarrow p(y)\}$. Avec les conditions de renommage issues de [8, 78, 82], on peut construire la dérivation suivante :

$$p(z) \xrightarrow{C_1, \{z/f(x)\}} p(y) \xrightarrow{C_2, \{y/f(x)\}} p(z) \rightarrow \dots$$

où $C_1$ est la clause $p(f(x)) \leftarrow p(y)$ et $C_2$ est la clause $p(f(x)) \leftarrow p(z)$. Si l'on considère à présent les conditions de renommage issues de [98], on ne peut plus utiliser la clause $C_2$

<footnote n="1">¹Dans tout ce document, les substitutions sont notées $\{x_1/t_1, \dots, x_n/t_n\}$ et dénotent la fonction qui étant donnée une variable $v$ retourne $t_i$ si $v = x_i$ et retourne $v$ sinon.</footnote>
lors de la deuxième transition puisque $z \in \text{var}(C_2) \cap \text{var}(p(z))$. On peut utiliser à la place la clause $p(f(x)) \leftarrow p(w)$, notée $C'_2$, et obtenir la dérivation :

$$p(z)^{C'_1, \{z/f(x)\}} \underset{p(y)}{\overset{C'_2, \{y/f(x)\}}{\rightleftharpoons}} p(w) \rightarrow \dots$$

Or, en utilisant les conditions de renommage issues de [7], cette clause $C'_2$ ne peut plus être utilisée puisque $x \in \text{var}(C_1) \cap \text{var}(C'_2)$. On peut utiliser à la place la clause $p(f(v)) \leftarrow p(w)$, notée $C''_2$, et obtenir la dérivation :

$$p(z)^{C'_1, \{z/f(x)\}} \underset{p(y)}{\overset{C''_2, \{y/f(v)\}}{\rightleftharpoons}} p(w) \rightarrow \dots$$

Si le renommage des clauses permet d'établir les propriétés fondamentales de la SLD-résolution, il est aussi nécessaire pour définir la sémantique opérationnelle des programmes logiques : ce renommage a au moins deux rôles. D'une part, il permet d'éviter un échec du mécanisme d'unification. Par exemple, soit $P$ le programme défini $\{p(f(x)) \leftarrow \}$ et $R$ la requête $p(x)$. Sans un renommage de la clause de $P$ en dehors des variables de $R$, l'unification de $p(x)$ avec $p(f(x))$ échoue. En effet, le "test d'occurrence" est une opération fondamentale de l'algorithme d'unification qui élimine les équations de la forme $x = t[x]$ (où $t[x]$ désigne un terme fonctionnel contenant la variable $x$) car elles n'ont pas de solutions sur les termes finis. D'autre part, le mécanisme de renommage garantit l'obtention d'une substitution résultat la plus générale. Par exemple, soit $P$ le programme $\{p(y) \leftarrow \}$ et $R$ la requête $p(x), p(y)$. Supposons que la clause de $P$ ne soit pas renommée et qu'à partir de $R$, le premier atome soit sélectionné. On obtient alors la dérivation :

$$p(x), p(y) \stackrel{\{x/y\}}{\underset{P}{\rightleftharpoons}} p(y) \rightarrow_P \Box$$

dont la réponse est $\rho_1 = \{x/y\}$. Le renommage de la clause de $P$ en dehors des variables apparaissant dans $R$ permet d'obtenir une réponse plus générale. En effet, si l'on renomme cette clause en $p(x_1) \leftarrow$ pour la première transition puis en $p(x_2) \leftarrow$ pour la deuxième transition, on obtient la dérivation :

$$p(x), p(y) \stackrel{\{x/x_1\}}{\underset{P}{\rightleftharpoons}} p(y) \stackrel{\{y/y_1\}}{\underset{P}{\rightleftharpoons}} \Box$$

dont la réponse est $\rho_2 = \{x/x_1, y/y_1\}$ et est plus générale que $\rho_1$.

Prendre en compte de manière explicite la "partie renommage" de la SLD-résolution complique évidemment les preuves des propriétés classiques de la programmation logique. Cependant, le processus de renommage doit être considéré comme une composante à part entière de la sémantique opérationnelle des programmes logiques. C'est lui qui permet d'établir des propriétés sur les variables apparaissant dans une dérivation. Ces propriétés sont essentielles et ne constituent pas un simple détail technique comme le montrent les exemples qui suivent.

**Lemme de généralisation** Le lemme de généralisation, préliminaire au théorème de complétude de la SLD-résolution, s'énonce habituellement comme suit :

(Lifting lemma [7]) Let $P$ be a program, $N$ a goal and $\theta$ a substitution.
Suppose that there exists an SLD-refutation of $P \cup \{\theta N\}$ with the sequence of
mgu's $\theta_0, \dots, \theta_n$. Then, there exists an SLD-refutation of $P \cup \{N\}$ with the
sequence of mgu's $\theta'_0, \dots, \theta'_n$ such that $\theta'_n \dots \theta'_0$ is more general than $\theta_n \dots \theta_0 \theta$.
Aucune hypothèse sur la substitution $\theta$ n'est posée dans cet énoncé. Néanmoins, si l'on veut pouvoir utiliser exactement les mêmes variantes de clauses dans les deux dérivations, ce qui est toujours implicitement suggéré, certaines hypothèses sont nécessaires.

En effet, soit $C_1$ la variante de clause utilisée lors de la première étape de résolution de la dérivation en hypothèse du lemme. Tandis que les conditions de renommage de $C_1$ stipulent que $C_1$ ne partage pas de variables avec la requête $\theta N$, il faut, pour pouvoir construire la dérivation en conclusion du lemme, que $C_1$ ne partage pas non plus de variables avec $N$. Or, sans aucune hypothèse supplémentaire, il se peut très bien qu'une variable de $N$ n'apparaisse pas dans $\theta N$ et soit donc présente dans $C_1$. Par exemple, si $P$ est le programme $\{p(f(v), f(z)) \leftarrow\}$, $N$ le but $\leftarrow p(f(a), y)$ et $\theta$ est la substitution $\{y/f(x)\}$, alors à partir du but initial $\theta N = \leftarrow p(f(a), f(x))$, rien n'empêche de renommer la clause de $P$ à l'aide de la substitution de renommage $r = \{z/y\}$ et d'obtenir la dérivation :

$$ \underbrace{p(f(a), f(x))}_{\theta N} \overset{\{v/a, x/y\}}{\rightarrow_P} \Box $$

Considérons à présent la dérivation que l'on peut obtenir à partir du but $N$: la clause de $P$ doit être renommée *en dehors* des variables de $N$. La substitution de renommage $r$, utilisée dans la dérivation précédente ne convient donc plus, puisqu'elle renomme $z$ en $y$ qui apparaît dans $N$. En effet, lors de la dérivation à partir de $\theta N$, le renommage de la clause $C$ utilisée satisfait seulement $var(\theta N) \cap var(rC) = \emptyset$ alors que la construction d'une dérivation à partir de $N$ nécessite la condition $var(N) \cap var(rC) = \emptyset$. Aussi, pour pouvoir prouver formellement le lemme de généralisation, il faut supposer que la clause $C$ utilisée est renommée *en dehors* des variables de $N$ à chaque transition.

D'autres précautions à prendre concernent le lien que doit entretenir la substitution $\theta$ avec $N$. En effet, si $\theta$ affecte des variables non présentes dans $N$, quelques problèmes peuvent apparaître. Par exemple, si $P$ est le programme $\{p(f(y), f(z)) \leftarrow\}$, $N$ le but $\leftarrow p(f(a), y)$ et $\theta$ la substitution $\{x/w\}$, alors on peut renommer la clause de $P$ à l'aide de la substitution de renommage $r = \{y/x\}$ et construire les dérivations :

$$ \underbrace{p(f(a), y)}_{\theta N} \overset{\rho_1 = \{x/a; y/f(z)\}}{\rightarrow_P} \Box \qquad \underbrace{p(f(a), y)}_{N} \overset{\rho_2 = \{x/a; y/f(z)\}}{\rightarrow_P} \Box $$

Cependant, $\rho_2 = \{x/a; y/f(z)\} \le \rho_1\theta = \{x/w; y/f(z)\}$ n'est pas vérifié. Pour éviter cette situation, il faut donc imposer que les clauses utilisées soient renommées *en dehors* des variables du domaine de $\theta$.

La formalisation que j'ai réalisée avec Coq a permis de mettre en évidence les hypothèses implicites sur le renommage des clauses lors de la dérivation en hypothèse du lemme de généralisation, hypothèses sans lesquelles il était bien sûr impossible de mécaniser la preuve.

**Lemme de commutation** Un problème similaire s'est posé lors de la preuve du lemme de commutation. Ce résultat classique, assurant que le choix de l'atome sélectionné lors d'une étape de résolution relève d'un non-déterminisme par indifférence (*don't care non-determinism*), s'énonce habituellement :
(Switching lemma [78]) If during a derivation, two atoms $L_1$ and $L_2$ are successively selected, then they can also be selected in the reverse order and the derived states are the same up to renaming of variables.

$$ \underbrace{(\dots, L_1, \dots, L_2, \dots)}_{R_0} \quad \begin{array}{c} C_1 \perp \quad \downarrow \\ \underbrace{\theta(\dots, C_1^-, \dots, L_2, \dots)}_{R_1} \quad \downarrow \quad \sigma(\dots, L_1, \dots, C_2^-, \dots) \end{array} \quad \begin{array}{c} C_2 \downarrow \\ \eta\theta(\dots, C_1^-, \dots, C_2^-, \dots) \approx \mu\sigma(\dots, C_1^-, \dots, C_2^-, \dots) \end{array} $$

Ici encore, quelques précautions sont nécessaires si l'on veut pouvoir utiliser les mêmes variantes des clauses $C_1$ et $C_2$ dans les deux dérivations (ce qui est habituellement suggéré dans la preuve de ce lemme). En effet, le renommage des clauses $C_1$ et $C_2$ dans la dérivation en hypothèse du lemme garantit normalement que $var(C_1) \cap var(R_0) = \emptyset$ et $var(C_2) \cap var(R_1) = \emptyset$. De plus les variables présentes dans la requête $R_1$ proviennent soit de la clause utilisée, soit de la requête $R_0$, et on a :

$$ \forall x \quad x \in var(R_1) \Rightarrow (x \in var(C_1) \lor x \in var(R_0)) \qquad (B.1) $$

Cependant, si l'on veut pouvoir sélectionner l'atome $L_2$, avant $L_1$, en utilisant la même variante de la clause $C_2$, il faut que cette variante soit telle que $var(C_2) \cap var(R_0) = \emptyset$. Or rien dans l'hypothèse du lemme de commutation ne garantit une telle propriété, et selon les conditions de renommage imposées dans la définition d'une dérivation, il est tout à fait possible qu'une variable présente dans la requête $R_0$, mais n'apparaissant pas dans $R_1$, ait été utilisée dans la variante de $C_2$. Pour contourner ce problème, et d'après (B.1), il faut que le renommage des clauses soit tel que $var(C_2) \cap var(C_1) = \emptyset$. C'est heureusement le cas si l'on utilise les hypothèses de renommage formulées dans [7] (i.e. du fait du renommage de la clause $C_i$ en dehors des clauses $C_0, C_1, \dots, C_{i-1}$) mais ce n'est plus le cas si l'on utilise les conditions énoncées dans [8, 78, 82, 84, 98] qui ne permettent donc pas de prouver formellement le lemme de commutation. Ici encore, c'est le travail de mécanisation des preuves qui a permis de mettre en évidence les propriétés de renommage requises pour obtenir la preuve avec Coq.

**Renommer une dérivation** Formaliser une preuve nous conduit donc à l'établir à un niveau de détail supérieur à celui généralement exposé. Dans le domaine de la programmation logique, un exemple typique de détail concerne le renommage de la clause utilisée lors d'une étape de résolution. La raison pour laquelle il est fréquent et admis de s'affranchir de ces détails est l'existence d'un lemme dû à J.W. Lloyd et J.C. Shepherdson [85], affirmant que si deux dérivations diffèrent seulement dans le choix des variables utilisées pour renommer les clauses (et par conséquent dans les unificateurs utilisés), alors les états dérivés sont équivalents à un renommage près des variables.

(Uniqueness) If two SLDNF-derivations differ only in the variants of clauses and the mgu which are used, then the resultants are variants of each other.

Autrement dit, l'existence d'une dérivation ne dépend pas du choix des variables de renommage : il suffit que de "bonnes" conditions de séparation des variables soit satisfaites.