LogoLogo

Brunel, Julien. Combinaison des logiques temporelle et déontique pour la spécification de politiques de sécurité

Brunel, Julien (2007). Combinaison des logiques temporelle et déontique pour la spécification de politiques de sécurité.

[img]PDF - nécessite un logiciel de visualisation PDF comme GSview, Xpdf or Adobe Acrobat Reader
1190Kb

Résumé en francais

Pour spécifier formellement une politique de sécurité, il est naturel de raisonner d'une part sur la notion de temps, et d'autre part sur les notions d'obligation, de permission, et d'interdiction. En effet, il s'agit d'exprimer par exemple le droit d'accès à une ressource pendant une certaine durée, l'obligation de la libérer avant un instant donné, ou encore l'obligation qu'une certaine tâche ne soit pas exécutée pendant un temps trop important. Les logiques temporelle et déontique apparaissent comme des outils adéquats pour spécifier de telles notions. Dans cette thèse, nous étudions comment combiner de telles logiques. Nous étudions dans un premier temps le produit de la logique temporelle linéaire avec la logique déontique standard, et définissons une obligation avec délai dans ce contexte. L'obligation avec délai doit notamment satisfaire une propriété que l'on nomme propagation: tant qu'elle n'est pas remplie et que le délai n'est pas atteint, elle se propage à l'instant suivant. Nous proposons ensuite une sémantique qui valide une propriété de propagation plus générale, puis définissons une axiomatique et une procédure de décision pour fragment du langage qui ne contient pas l'opérateur temporel 'until'. Nous nous intéressons enfin à la notion de conformité d'un système vis à vis d'une politique de sécurité spécifiée dans un tel langage. La première définition que nous proposons est une version faible de la conformité que l'on nomme compatibilité. Nous restreignons ensuite le langage afin définir une version plus forte de la conformité, et proposons un algorithme pour vérifier la conformité d'un système vis à vis d'une politique.

Sous la direction du :
Directeur de thèse
Bodeveix, Jean-Paul
Filali Amine, Mamoun
Ecole doctorale:Mathématiques, informatique, télécommunications de Toulouse (MITT)
laboratoire/Unité de recherche :Institut de Recherche en Informatique de Toulouse (IRIT), UMR 5505
Mots-clés libres :logique temporelle - logique déontique - politique de sécurité
Sujets :Informatique
Déposé le :30 Apr 2008 11:19