Combinaison des logiques temporelle et déontique pour la spécification de politiques de sécurité
Institution:
Toulouse 3Disciplines:
Directors:
Abstract EN:
In order to formally specify a security policy, it is natural to reason about time on the one hand, and obligations, permissions, and prohibitions on the other hand. Indeed, we have to express for instance the permission to access a resource for a certain period, the obligation to release a resource before a deadline, or the prohibition to execute a task for a too long period. Temporal and deontic logics seem well suited to specify such concepts. In this thesis, we study how to combine these logics. Firstly, we study the product of linear temporal logic and standard deontic logic, and define obligation with deadline in this context. It has to satisfy a property called propagation property: while it is not fulfilled, it is propagated to the next instant. We then propose a more general propagation property, and propose a semantics to validate it. For the until-free fragment of our logic, we define an axiomatics and a tableaux-like decision procedure. Lastly, we investigate the notion of compliance of a system with respect to a policy specified in such a language. The first definition we come up with is a weak version of compliance called compatibility. For a new fragment of our logic, we adapt the Büchi approach of Vardi and Wolper to decide whether a system is compliant with a policy. We then restrict again the language so that we can define a stronger version of compliance. Actually, a careful analysis shows the necessity to refine the notion of compliance into 5 different diagnostic cases which give 'levels of compliance'. We provide an algorithm to establish this diagnostic.
Abstract FR:
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.