Formal Specification and Validation of Security Policies

Tony Bourdier; Horatiu Cirstea; Mathieu Jaume; Hélène Kirchner

inria-00507300, version 2

Formal Specification and Validation of Security Policies

Tony Bourdier () ¹, Horatiu Cirstea () ¹, Mathieu Jaume ², Hélène Kirchner ()^a^, 1, 3

FPS - 4th Canada-France MITACS Workshop on Foundations and Practice of Security - 2011 6888 (2011) 148-163

Résumé : We propose a formal framework for the specification and validation of security policies. To model a secured system, the evolution of security information in the system is described by transitions triggered by authorization requests and the policy is given by a set of rules describing the way the corresponding decisions are taken. Policy rules are constrained rewrite rules whose constraints are first-order formulas on finite domains, which provides enhanced expressive power compared to classical security policy specification approaches like the ones using Datalog, for example. Our specifications have an operational semantics based on transition and rewriting systems and are thus executable. This framework also provides a common formalism to define, compare and compose security systems and policies. We define transformations over secured systems in order to perform validation of classical security properties.

a – CNRS
1 : PAREO (INRIA Lorraine - LORIA)
INRIA – CNRS : UMR7503 – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
2 : Laboratoire d'Informatique de Paris 6 (LIP6)
CNRS : UMR7606 – Université Pierre et Marie Curie [UPMC] - Paris VI
3 : INRIA Bordeaux - Sud-Ouest (INRIA Bordeaux - Sud-Ouest)
INRIA

inria-00507300, version 2
http://hal.inria.fr/inria-00507300
oai:hal.inria.fr:inria-00507300
Contributeur : Tony Bourdier <>
Soumis le : Mardi 22 Février 2011, 09:01:02
Dernière modification le : Lundi 7 Janvier 2013, 17:16:43

Voir la fiche détaillée

Documents associés

PDF :

DOI : 10.1007/978-3-642-27901-0_12

Exporter

Bibtex EndNote TEI RefWorks

%% inria-00507300, version 2
%% http://hal.inria.fr/inria-00507300
@inproceedings{bourdier:inria-00507300,
    hal_id = {inria-00507300},
    url = {http://hal.inria.fr/inria-00507300},
    title = {{Formal Specification and Validation of Security Policies}},
    author = {Bourdier, Tony and Cirstea, Horatiu and Jaume, Mathieu and Kirchner, H{\'e}l{\`e}ne},
    abstract = {{We propose a formal framework for the specification and validation of security policies. To model a secured system, the evolution of security information in the system is described by transitions triggered by authorization requests and the policy is given by a set of rules describing the way the corresponding decisions are taken. Policy rules are constrained rewrite rules whose constraints are first-order formulas on finite domains, which provides enhanced expressive power compared to classical security policy specification approaches like the ones using Datalog, for example. Our specifications have an operational semantics based on transition and rewriting systems and are thus executable. This framework also provides a common formalism to define, compare and compose security systems and policies. We define transformations over secured systems in order to perform validation of classical security properties.}},
    keywords = {Security policies; formal specification; formal validation; constrained rewriting systems},
    language = {Anglais},
    affiliation = {PAREO - INRIA Lorraine - LORIA , Laboratoire d'Informatique de Paris 6 - LIP6 , INRIA Bordeaux - Sud-Ouest - INRIA Bordeaux - Sud-Ouest},
    booktitle = {{FPS - 4th Canada-France MITACS Workshop on Foundations and Practice of Security - 2011}},
    publisher = {Springer, Heidelberg},
    pages = {148-163},
    address = {Paris, France},
    volume = {6888},
    editor = {J. Garcia-Alfaro and P. Lafourcade },
    series = {Lecture Notes in Computer Science },
    audience = {internationale },
    doi = {10.1007/978-3-642-27901-0\_12 },
    year = {2012},
    pdf = {http://hal.inria.fr/inria-00507300/PDF/FormalSpecificationandValidationofSecurityPolicies.pdf},
}

<?xml version="1.0" encoding="UTF-8"?>
<listBibl xmlns="http://www.tei-c.org/ns/1.0" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mml="http://www.w3.org/1998/Math/MathML">
<listBibl type="inproceedings"><head>Communications avec actes</head>
<biblStruct type="inproceedings" xml:id="inria-00507300"><analytic>
<author><persName><forename>Tony</forename><surname>Bourdier</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Lorraine - LORIA</orgName>
<orgName type="team">PAREO</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : UMR7503</orgName>
<orgName type="institution">Université Henri Poincaré - Nancy I</orgName>
<orgName type="institution">Université Nancy II</orgName>
<orgName type="institution">Institut National Polytechnique de Lorraine (INPL)</orgName>
</affiliation>
</author>
<author><persName><forename>Horatiu</forename><surname>Cirstea</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Lorraine - LORIA</orgName>
<orgName type="team">PAREO</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : UMR7503</orgName>
<orgName type="institution">Université Henri Poincaré - Nancy I</orgName>
<orgName type="institution">Université Nancy II</orgName>
<orgName type="institution">Institut National Polytechnique de Lorraine (INPL)</orgName>
</affiliation>
</author>
<author><persName><forename>Mathieu</forename><surname>Jaume</surname></persName>
<affiliation>
<orgName type="laboratory">LIP6</orgName>
<orgName type="team">Laboratoire d'Informatique de Paris 6</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR7606</orgName>
<orgName type="institution">Université Pierre et Marie Curie [UPMC] - Paris VI</orgName>
</affiliation>
</author>
<author><persName><forename>Hélène</forename><surname>Kirchner</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Lorraine - LORIA</orgName>
<orgName type="team">PAREO</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : UMR7503</orgName>
<orgName type="institution">Université Henri Poincaré - Nancy I</orgName>
<orgName type="institution">Université Nancy II</orgName>
<orgName type="institution">Institut National Polytechnique de Lorraine (INPL)</orgName>
</affiliation>
<affiliation>
<orgName type="laboratory">INRIA Bordeaux - Sud-Ouest</orgName>
<orgName type="team">INRIA Bordeaux - Sud-Ouest</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
</affiliation>
</author>
<title type="main" level="a">Formal Specification and Validation of Security Policies</title></analytic><monogr><meeting>FPS - 4th Canada-France MITACS Workshop on Foundations and Practice of Security - 2011</meeting><imprint><publisher>Springer, Heidelberg</publisher><pubPlace><settlement>Paris</settlement><country>France</country></pubPlace><biblScope type="publicationDate">2012-00-00</biblScope><biblScope type="vol">6888</biblScope><biblScope type="pp">148-163</biblScope></imprint></monogr><idno type="doi">10.1007/978-3-642-27901-0_12</idno><idno type="HALid">http://hal.inria.fr/inria-00507300</idno><idno type="HALFile">http://hal.inria.fr/inria-00507300/PDF/FormalSpecificationandValidationofSecurityPolicies.pdf</idno></biblStruct>
</listBibl>
</listBibl>