Formalisation de propriétés de sécurité pour la protection des systèmes d'exploitation
Cette thèse traite du problème d une protection en profondeur qui puisse être assurée par un système d exploitation. Elle établit la faiblesse des solutions existantes pour l expression des besoins de sécurité. Les approches supportent en général une seule propriété de sécurité. Nous proposons donc...
محفوظ في:
| المؤلف الرئيسي: | |
|---|---|
| مؤلفون آخرون: | |
| التنسيق: | Thèse numérique |
| اللغة: | Français |
| منشور في: |
2010.
|
| الموضوعات: | |
| الوصول للمادة أونلاين: | Accès au texte intégral https://theses.univ-orleans.fr/public/2010ORLE2075_vm.pdf http://www.theses.fr/2010ORLE2075/abes https://theses.hal.science/tel-00623075 |
| ملاحظة: |
Titre provenant de l'écran-titre Ecole(s) Doctorale(s) : École doctorale Sciences et technologies (Orléans ; 2009-2012) Partenaire(s) de recherche : Laboratoire d'informatique fondamentale d'Orléans (Orléans ; 1987-....) (Laboratoire), Laboratoire d'Informatique Fondamentale d'Orléans (Laboratoire) Autre(s) contribution(s) : Sébastien Limet (Président du jury) ; Christian Toinard, Sébastien Limet, Francine Krief, Jean-Yves Marion, Patrice Clemente, Mathieu Blanc (Membre(s) du jury) ; Francine Krief, Jean-Yves Marion (Rapporteur(s)) |
| Autres localisations: | Voir dans le Sudoc |
| Variante du titre: | Security properties formalization for operating system protection |
| LEADER | 05129nam a22003737a 4500 | ||
|---|---|---|---|
| 001 | 405511 | ||
| 008 | 110913s2010 xxe ||| |||| 00| 0 fre d | ||
| 009 | PPN15483002X | ||
| 041 | 0 | |a fre |b fre |b eng | |
| 084 | |a 004 | ||
| 100 | 1 | |a Rouzaud-Cornabas, Jonathan. | |
| 240 | 1 | 0 | |a Security properties formalization for operating system protection |
| 245 | 1 | 0 | |a Formalisation de propriétés de sécurité pour la protection des systèmes d'exploitation |c Jonathan Rouzaud-Cornabas ; sous la direction de Christian Toinard. |
| 256 | |a Données textuelles | ||
| 260 | |c 2010. | ||
| 500 | |a Titre provenant de l'écran-titre | ||
| 500 | |a Ecole(s) Doctorale(s) : École doctorale Sciences et technologies (Orléans ; 2009-2012) | ||
| 500 | |a Partenaire(s) de recherche : Laboratoire d'informatique fondamentale d'Orléans (Orléans ; 1987-....) (Laboratoire), Laboratoire d'Informatique Fondamentale d'Orléans (Laboratoire) | ||
| 500 | |a Autre(s) contribution(s) : Sébastien Limet (Président du jury) ; Christian Toinard, Sébastien Limet, Francine Krief, Jean-Yves Marion, Patrice Clemente, Mathieu Blanc (Membre(s) du jury) ; Francine Krief, Jean-Yves Marion (Rapporteur(s)) | ||
| 502 | |a Thèse de doctorat. Informatique. Orléans. 2010 | ||
| 520 | |a Cette thèse traite du problème d une protection en profondeur qui puisse être assurée par un système d exploitation. Elle établit la faiblesse des solutions existantes pour l expression des besoins de sécurité. Les approches supportent en général une seule propriété de sécurité. Nous proposons donc un langage qui permet de formaliser un large ensemble de propriétés de sécurité. Ce langage exprime les activités système directes et transitives. Il permet de formaliser la majorité des propriétés de confidentialité et d intégrité de la littérature. Il est adapté à l expression de modèles de protection dynamique. A titre d exemple, un nouveau modèle dynamique est proposé pour la protection des différents domaines d usage d un navigateur Web. Nous définissons une méthode de compilation du langage pour analyser les appels systèmes réalisés par les processus utilisateurs. La compilation repose sur la construction et l analyse d un graphe de flux d information. Nous montrons qu en pratique la complexité reste faible. Une implantation de ce langage est proposée sous la forme d un contrôle d accès mandataire dynamique pour Linux. Une expérimentation à large échelle a été réalisée sur des pots-de-miel à haute interaction. Notre protection a montré son efficacité aussi bien pour les serveurs que les postes client. Il présente des perspectives intéressantes aussi bien pour la protection des systèmes que pour l analyse de vulnérabilités. Ce travail a contribué au projet SPACLik vainqueur du défi sécurité de l ANR SEC&SI. | ||
| 520 | |a The subject of this thesis is to propose an in-depth protection that can be enforced by the operating system. First, we present that current security solutions are weak in the expression of security. Indeed, most of them support only one security properties. We introduce a language that allows to formalize a large set of security properties. This language expresses directs and transitives system activities. It allows to formalize the majority of integrity and confidentiality security properties introduced in the litterature. Moreover, the language can also expresses dynamic security properties. We introduces a new dynamic security model for the protection of multiple security domains managed by a web browser. We define a method to compil our language. The purpose is to analyze the system call done by the users processes. The compilation process build and analyze an information flow graph. Futhermore, we show that the complexity of our protection solution is low. We propose an implementation of this language as a dynamic mandatory access control for Linux. We experiment it on large scale high interaction honeypots. Our protection shows its efficiency both for clients and servers. Moreover, it presents interesting perspectives for the protection of other systems and for the vulnerability analysis. This work has contributed to the SPACLik project that wins the security contest of the French National Research Agency : ANR SEC&SI. | ||
| 538 | |a Configuration requise : un logiciel capable de lire un fichier au format : PDF | ||
| 650 | |a Systèmes d'exploitation (ordinateurs) | ||
| 650 | |a Systèmes informatiques |x Mesures de sûreté | ||
| 650 | |a Ordinateurs |x Accès |x Contrôle | ||
| 650 | |a Thèses et écrits académiques | ||
| 700 | 1 | |a Toinard, Christian. |4 ths |4 opn | |
| 710 | 2 | |a Université d'Orléans. |4 dgg | |
| 856 | 4 | |q PDF |s 2905768 |u http://www.theses.fr/2010ORLE2075/document |z Accès au texte intégral | |
| 856 | 4 | |u https://theses.univ-orleans.fr/public/2010ORLE2075_vm.pdf | |
| 856 | 4 | |u http://www.theses.fr/2010ORLE2075/abes | |
| 856 | 4 | |u https://theses.hal.science/tel-00623075 | |
| 997 | |0 405511 |1 Thèse numérique |a Ressource numérique |b INSA |b ENSA |c 0/Bibliothèque numérique/ |c 1/Bibliothèque numérique/Autre ressource numérique/ | ||