Security for Cloud Environment through Information Flow Properties Formalization with a First-Order Temporal Logic

Arnaud Lefray 1 Jonathan Rouzaud-Cornabas 2 Jérémy Briffaut 3 Christian Toinard 3
2 AVALON - Algorithms and Software Architectures for Distributed and HPC Platforms
Inria Grenoble - Rhône-Alpes, LIP - Laboratoire de l'Informatique du Parallélisme
3 SDS
LIFO - Laboratoire d'Informatique Fondamentale d'Orléans
Résumé : La principale cause de ralentissement de l'adoption du Cloud est le manque de sécurité fiable. Le concept de sécurité à la demande est de déployer et d'appliquer les demandes de sécurité d'un client. Dans ce papier, nous présentons une approche, Information Flow Past Linear Time Logic (IF-PLTL), qui permet de spécifier comment un système peut supporter un large ensemble de propriétés de sécurité. Nous présentons dans ce papier comment ces flux d'information peuvent être contrôler en utilisant les événements systèmes de bas niveau. Nous donnons une description compléte de la syntaxe de IF-PLTL ainsi que sa sémantique. De plus, cette logique permet de formaliser un large ensemble de politiques de sécurité. Notre approche est illustrée par la politique de sécurité de la muraille de Chine orienté vers le monde commercial. Finalement, nous montrons comment nous avons étendu notre langage pour supporter la relabélisation dynamique qui permet de supporter la dynamicité inhérante des systèmes. Nous illustrons cette extension par la formalisation d'une propriété de sécurité pour l'isolation dynamique de domaines.
Liste complète des métadonnées

https://hal.inria.fr/hal-00916882
Contributeur : Jonathan Rouzaud-Cornabas <>
Soumis le : mardi 10 décembre 2013 - 20:39:24
Dernière modification le : vendredi 20 avril 2018 - 15:44:26
Document(s) archivé(s) le : vendredi 14 mars 2014 - 10:15:59

Fichiers

RR-8420.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00916882, version 1

Citation

Arnaud Lefray, Jonathan Rouzaud-Cornabas, Jérémy Briffaut, Christian Toinard. Security for Cloud Environment through Information Flow Properties Formalization with a First-Order Temporal Logic. [Research Report] RR-8420, INRIA. 2013, pp.30. 〈hal-00916882〉

Partager

Métriques

Consultations de la notice

479

Téléchargements de fichiers

379