On Formal Specification and Analysis of Security Policies
| Autor: | Bourdier, Tony, Cirstea, Horatiu, Jaume, Mathieu, Kirchner, Hélène |
|---|---|
| Přispěvatelé: | Formal islands: foundations and applications (PAREO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS), Sémantiques, preuves et implantation (SPI), Laboratoire d'Informatique de Paris 6 (LIP6), Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS), Inria Bordeaux - Sud-Ouest, Institut National de Recherche en Informatique et en Automatique (Inria), ANR-06-SETI-0016,SSURF,Sûreté et sécurité avec focal(2006), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP) |
| Jazyk: | angličtina |
| Rok vydání: | 2010 |
| Předmět: | |
| Zdroj: | 2010 Grande Region Security and Reliability Day 2010 Grande Region Security and Reliability Day, Mar 2010, Saarbrücken, Germany |
| Popis: | International audience; Security policies are ubiquitous in information systems and more generally in the management of sensitive information. Access control policies are probably the most largely used policies but their application goes well beyond this application domain. The enforcement of security policies is useless if some of their key properties like the consistency, for example, cannot be stated and checked. We propose here a framework where the security policies and the systems they are applied on, are specified separately but using a common formalism. This separation allows us not only some analysis of the policy independently of the target system but also the application of a given policy on different systems. Besides the abstract formalism we also explore how rewrite and reduction systems can be used and combined in a rather systematic way to provide executable specifications for this framework. We also propose a notion of system and policy transformation that gives the possibility to study some properties which cannot be expressed only within the initial presentation. We have shown, in particular, how confidentiality, integrity and confinment can be expressed for the BLP policy that does not deal explicitly with information flows but only with objects containing tractable information. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|