Romuald Thion
email: romuald.thion@univ-lyon1.fr

Stéphane Coulondre
email: stephane.coulondre@insa-lyon.fr

A Relational Database Integrity Framework for Access Control Policies

Keywords: Integrity Model, Dependencies, Authorization, Access Control, Inference

Access control is one of the most common and versatile mechanisms used for information systems security enforcement. An access control model formally describes how to decide whether an access request should be granted or denied. Since the rolebased access control initiative has been proposed in the 90s, several access control models have been studied in the literature.

An access control policy is an instance of a model. It denes the set of basic facts used in the decision process. Policies must satisfy a set of constraints dened in the model, which reect some high level organization requirements. First-order logic has been advocated for some time as a suitable framework for access control models. Many frameworks have been proposed, focusing mainly on expressing complex access control models. However, though formally expressed, constraints are not dened in a unied language that could lead to some well-founded and generic enforcement procedures.

Therefore, we make a clear distinction by proposing a logical framework focusing primarily on constraints, while keeping as much as possible a unied way of expressing constraints, policies, models, and reference monitors. This framework is closely tied to relational database integrity models. We then show how to use well-founded procedures in order to enforce and check constraints. Without requiring any rewriting previous to the inference process, these procedures provide clean and intuitive debugging traces for administrators. This approach is a step toward bridging the gap between general but hard to maintain formalisms and eective but insuciently general ones.

Introduction

1.1 Access control models, policies and constraints Security policies are sets of laws and rules governing the security of organizations.

They can cover areas from internal organizations rules to national laws, from structural (e.g., re protection) to organizational aspects (e.g., emergency phone lines). An Access Control (ac) (or authorization) policy is a specialized form of security policy, dedicated to permission management. ac aims at enforcing condentiality and data integrity.

Within information systems, an ac policy is structured according to an ac model, which formally describes the structure of the policy. A model denes how to decide whether an access request (i.e., an action on an object issued by a subject pertaining to a user) should be granted or denied using a set of rules. For instance, in the Role-Based Access Control (Rbac) models family, roles are assigned to users, and permissions are assigned to roles [START_REF] Sandhu | Role-based access control models[END_REF][START_REF] Ferraiolo | Role-Based Access Control[END_REF]. An Rbac policy is a set of assignments between users and roles and between roles and permissions. The core rule of the Rbac models family states that an access request is granted if and only if the issuer endorses a role with this privilege.

Since the Rbac initiative, several models have been studied in the literature.

These models have extended Rbac (e.g., Generalized-Temporal -Rbac [START_REF] Joshi | A generalized temporal role-based access control model[END_REF] or Geographical -Rbac [START_REF] Maria | GEO-RBAC: A spatially aware rbac[END_REF]), and have organized policies by additional concepts to enhance their expressive power and exibility (e.g., Workow-Rbac [START_REF] Wainer | W-RBAC -a workow security model incorporating controlled overriding of constraints[END_REF][START_REF] Wainer | DW-RBAC: A formal security model of delegation and revocation in workow systems[END_REF], Team -Bac (Thomas, 1997), Task -Bac [START_REF] Thomas | Task-based authorization controls (TBAC): A family of models for active and enterprise-oriented autorization management[END_REF], Organization -Bac [START_REF] Miège | Dénition d'un environnement formel d'expression de politiques de sécurité : modèle Or-BAC et extensions[END_REF]). Throughout these propositions, First-Order Logic (Fol) has been advocated as a general framework suitable to formalize ac models and policies.

In addition to innovative concepts and relations (e.g., roles and hierarchies) for organizing policies, ac models have integrated the concept of constraints. Constraints reect some high level organization requirements that must be enforced within policies.

With the development of ac models, several kinds of constraints have been dened.

The most prominent one is the mutual exclusion, which has been proposed in order to enforce separation of duties [START_REF] Li | On mutually-exclusive roles and separation of duty[END_REF]. Other kinds of constraints have been dened: some mutual exclusion variants, prerequisite constraints or constraints over hierarchies [START_REF] Crampton | Specifying and enforcing constraints in role-based access control[END_REF][START_REF] Jaeger | Practical safety in exible access control models[END_REF].

Actually, constraints may express dierent requirements on policies. Generally speaking, constraints are policy properties that can be classied in the following basic classes:

(conditional) absence of values (e.g., mutual exclusion), (conditional) existence of (constrained) values (e.g., prerequisite), (conditional) uniqueness of values (e.g., uniqueness of ancestor in a hierarchy).

These dierent classes of constraints share a common objective, which is to restrict the set of policies expressible over a model to the set of consistent ones. For instance, in the Rbac setting, the denition of roles a and b as mutually exclusive means that no user should be assigned to a and b. Thus, the set of expressible policies is restricted to the set of policies in which no user is assigned to both a and b.

Problem statement and contribution

Constraints attempt to ensure that policies are consistent. Verifying the consistency of policies is a paramount task. Indeed an inconsistent policy can lead to an unexpected behaviour of the ac system that may completely ruin the benets of the ac system: illegitimate access: exclusion constraints aim at ensuring that some activities are carried out by dierent users, for instance to prevent that the same user from initiating a payment and authorizing a payment. If a policy does not satisfy the exclusion constraints, one unique user may be able to circumvent the separation of duties and gain unlegitimate access, deny of legitimate access: conversely, a constraint can express that every user has the right to log into the system. Failing to verify such a constraint may lead to users to be unable to do anything, dierence between expected behaviour and real behaviour: some constraints are implicitly expected from a model. For instance, when dealing with a role hierarchy, it is relevant and quite natural to prevent graph cycles. Failing to verify such constraint may lead to circular inheritance that implies that all the roles have the same set of permissions. Moreover, in a Rbac setting, such a set would be the union of all permissions assigned to at least one role in the cycle, unpredictable behaviour: in the worst case, if core constraints like basic integrity requirements of policy (e.g., uniqueness of user related to a subject) are not satised, the whole system may be compromised.

In order to express these constraints in an homogeneous way, a formal language able to handle broad classes of constraints is necessary. It should allow the denition of new classes of constraints and should be able to capture general integrity requirements of ac models. This language must have clear semantics, and provide well-founded automated proof procedures for consistency checking.

To address these issues we adopt a top-down approach, starting with a framework focusing primarily on constraints. This framework relies on database integrity theory.

We have chosen to present it in a logical setting, but other formalisms, such as tableaux, could have been used. ac models and policies are then formally dened using one of the Datalog languages, which is also a fragment of the database integrity language. This interesting property allows for expressing the whole ac system, including models, policies and constraints, in a single and homogeneous framework. ac models foundations and semantics are described in section 2. Without being universal, the obtained framework can still express several classical models and extensions found in the literature.

We then dene ac constraints in section 3. We make use of relational data dependencies, in order to model ac constraints. Dependencies are able to capture complex integrity requirements in an homogeneous way. For instance, one of the properties considered as fundamental in the Rbac standard (Ferraiolo et al., 2003, property 3.2, p.60) (this property is quoted in section 3.5) can be modelled by means of data dependencies.

To the best of our knowledge, the property (3.2) has not been modelled and taken into account in any other logical framework for ac.

In section 4, we dene a set of well-founded operations that can be used to help ac models designers and policy administrators in making constraints design and administration easier. These operations are generic and can be used over any model built upon the structure dened in sections 2 and 3.

We have implemented the framework and validated our approach with automated formal proofs based on previous results in the literature that had been manually proved.

These results are presented in section 4.6. Moreover, the proofs obtained are quite readable as no prior rewriting is performed (such as clausal form), for it may obfuscate human analysis.

Our approach tries to encompasses many concepts found in the ac literature, but it does not take into account some peculiarities of very dedicated models. For instance, our framework does not encompass authentication [START_REF] Jim | SD3: A trust management system with certied evaluation[END_REF] and delegation (Li et al., 2003;[START_REF] Wainer | DW-RBAC: A formal security model of delegation and revocation in workow systems[END_REF]. Section 6 evaluates the major design decisions of the framework. The very last section concludes this paper and gives the main directions for future work. For sake of clarity and applicability, most of the examples of in this paper are based upon the Rbac model and further extensions.

Access Control Framework

This section denes an access control framework able to express several classical models and extensions found in the literature. As we will see in the next section, this framework is a subset of the general framework proposed for access control constraints, that relies on database integrity theory.

Without lack of generality, we operate a clear distinction between models and policies : ac models denes structures and ac policies are instances of these structures. In such a perspective, ac design is the task of dening ac models, whereas administration of ac is the task of dening policies, which is up to administrators.

Fol has been advocated a suitable formal framework to formalize ac models and policies (Li et al., 2003;[START_REF] Jim | SD3: A trust management system with certied evaluation[END_REF][START_REF] Detreville | a logic-based security language[END_REF][START_REF] Bertino | A logical framework for reasoning about access control models[END_REF][START_REF] Li | DATALOG with constraints: A foundation for trust management languages[END_REF][START_REF] Barker | Flexible access control policy specication with constraint logic programming[END_REF][START_REF] Halpern | Using rst-order logic to reason about policies[END_REF][START_REF] Miège | Dénition d'un environnement formel d'expression de politiques de sécurité : modèle Or-BAC et extensions[END_REF].

From the logical point of view, an ac model both dene : a vocabulary, i.e., the set of sorts and relations between sorts used to organize access privileges (e.g, subjects, roles, permissions, assignments of roles to subjects) a set of so-called rules expressed in a rst-order language built over the vocabulary, i.e., the policy that states how privileges are derived from base concepts and relations (e.g., a subject is granted some access only if it endorses some role with the corresponding access right).

Section 2.1 denes the vocabulary and states of an ac model. Section 2.2 denes rules and policies. The generic denition of an ac model is summarized in section 2.3.

Access control vocabulary and state

An ac model relies on vocabulary : a set of sorts and relations between sorts. Sorts are the main concepts used to organize rights (e.g., users and roles. . . ). Relations dene how sorts are related in the model (e.g., assignments between users and roles). The goal of an ac system is to determine whether an access (an action on an object) issued by a subject that represents a user is granted or not. Thus, the main sorts of subjects, users, actions and objects have to be dened in any ac model. Sorts partition the set of constants in a policy. This property is tied to the manysorted Fol framework. It is shown that many-sorted Fol can be reduced to onesorted Fol (i.e., classical logic) by assigning a specic unary predicate symbol D S Fig. 1 The core vocabulary edb of Rbac. called domain predicate symbols to each sort S (Gallier, 1986, chapter 10, p. 460). In our framework, we implicitly operate this transformation by assigning a unique unary predicate symbol to each sort. The vocabulary is represented in the relational formalism according to the standard terminology used in databases.

Denition 1 Access control vocabulary. The vocabulary V oc of an ac model is the union of a set Sorts of unary predicate symbols called sorts and a set Rels of n-ary predicate symbols called relations.

The sorts of users (U ser), subjects (Subject), actions (Action) and objects (Object) must be present in any ac vocabulary.

Figure 1 illustrates the core vocabulary of Rbac models. This vocabulary is composed of ve sorts (drawn by rectangles in gure 1): U ser, Subject, Role, Action and Object. Moreover, four relations are dened (drawn by diamonds in gure 1): U RA betwen U ser and Role, P RA between Role, Action and Object, SU between Subject and U ser and SR between Subject and Role.

We dene the state of an ac model, which is a set of facts dened over the core vocabulary edb. The state of an ac model is the extensive part of a policy, which can practically be stored in a Relational Database Management System (rdbms). Following traditional axioms of logical interpretation of relational databases, we assume that constants are distinct and that states are nite.

Denition 2 Access control state. To each sort S ∈ Sorts is associated a set of constants S called its domain. Domains are pairwise disjoint: S ∩ S = ∅ for all S = S in Sorts. To each relation R ∈ Rels of arity n between sorts S 1 . . . Sn, is associated the set R = S 1 × . . . × Sn. An access control state I on an ac vocabulary V oc is a mapping from each sort S ∈ Sorts to a nite subset of S, called its active domain, and from each relation R ∈ Rels to a nite subset of R.

In the context of Rbac, the term ac state (a.k.a. Rbac database ) has rst been coined by [START_REF] Serban | Formal specication for role based access control user/role and role/role relationship management[END_REF]. A toy sample of an Rbac state I (over vocabulary shown in gure 1) is given in table 1. In this state, the sort U ser takes its values from the set {Alice, Bob, Charly}, Role from {r 1 , r 2 , r 3 , r 4 }, Action from {r, w, x} and Object from {file1, file2, file3}

In this state, Bob is assigned both roles r 1 and r 3 and Bob endorses these roles in two dierent sessions, namely S2 and S3. The rules of Rbac models allow inferring that Bob can read file1, file2 and file3 as the role r 1 is granted r access on file1, file2 and file3.

Access control rules and policies

In this section we dene the ac rules. Rules express the deductive principles of an ac model. From a set of rules P and a state I, it is possible to compute derived relations on which the access decision process is based. The state is the minimal knowledge from which a complete policy may be derived using the set of rules.

For instance, in order to prevent administrators from inserting redundancies in a policy, several algebraic properties of relations are commonly assumed: transitivity, reexivity or symmetry for instance. These properties are expressed in intenso by means of rules. Thus, administators only have to insert the minimal knowledge in the state. The complete policy is obtained by applying the set of rules P as a closure operator producing new facts.

In the case of complex ac models, dening derived relations within the model is a mandatory prerequisite in order to obtain a maintainable state. This separation between extensive relations in the state and intensive relations in the policy is a design choice made according to the recommendations addressed to the Rbac standard [START_REF] Li | A critique of the ANSI standard on rolebased access control[END_REF], in particular the third suggestion :

Suggestion 3: The standard should make a clear distinction between base relations and derived relations.

Several fragments of Fol have been used as formal languages for modelling ac rules. Datalog-based models are considered expressive enough to capture complex ac policies [START_REF] Bertino | A logical framework for reasoning about access control models[END_REF], [START_REF] Miège | Dénition d'un environnement formel d'expression de politiques de sécurité : modèle Or-BAC et extensions[END_REF], [START_REF] Jim | SD3: A trust management system with certied evaluation[END_REF], [START_REF] Barker | Flexible access control policy specication with constraint logic programming[END_REF].

We focused our work on Fol rules of Datalog C , which has been recognized as fruitful to formalize ac models [START_REF] Li | DATALOG with constraints: A foundation for trust management languages[END_REF].

We operate the main following specializations on Fol by selecting Datalog C as a formal language for rules: functions, negation and disjunction are not allowed. Formally, Datalog C sentences are formal expressions of the form:

∀ X R 1 (X 1 ) ∧ . . . ∧ Rn(Xn) ∧ ψ( X) ⇒ R 0 (X 0 )
where ∀i ∈ 0..n, R i are symbols from V oc and X i are sequences of logic variables of length equal to the arity of R i . The left-hand side of a rule (R 1 (X 1 ) ∧ . . . ∧ Rn(Xn) ∧ ψ( X)) is called the body of the rule its right-hand side (R 0 (X 0 )) is called its head. X is the set of variables that appear in the body. ψ( X) is a conjunction of linear arithmetic constraints (e.g., ≤, ≥, =, =) over variables and constants of same sorts.

Denition 3 Access control rules. The rules of and ac model is a set P of Datalog C sentences.

P denes a partition on the vocabulary V oc: idb ∩ edb = ∅ and idb ∪ edb = V oc. idb, for intensive database, is the set of relations that appear in the heads of the rules and edb, for extensive database, is the set of relations that appear only in the bodies of the rules but not in their heads.

The denition of the component P that captures rules is generic. It encompasses the main notions introduced in the literature to organize ac policies. Next subsections focus on three main derived relations that are commonly used in ac models : authorization triple, hierarchies and mutual exclusion. We can now formally dene ac policies.

Denition 4 Access control policy. The semantics of rules is given by the standard Fol model-theoretic interpretation of Datalog C rules.

Given an ac state I of a model AC = (V oc, P ), an access control policy I over a given state I is a logical model of P stated I |= P with I ⊆ I .

The existence of a decidable procedure which computes the interpretation I from I ensures that it is always possible to compute the policy and consequently to answer whether an access request is granted or denied. Datalog's (and its major extension such as Datalog C , C-Datalog or Datalog ¬ ) restrictions ensure that there is a unique minimal model of P and that this model can be computed in a nite time (Abiteboul et al., 1995, theorem 12.5.2, p. 301). Uniqueness of the minimal model ensures that for given state and set of rules there is a unique derived policy. The nite time property ensures that computation of the policy if decidable and thus, it ensures that access control requests will be always answered.

Derivation of authorizations

We have dened the structure of an ac model, however deriving authorizations from state has not been explained yet. As coined by Lampson in his seminal paper [START_REF] Butler | [END_REF], the aim of access control is to take a boolean ac decision upon an ac request. An ac request is a triple subject, action, and object. The reference monitor which enforces ac acts as a Non-bypassable, Evaluatable, Always Invoked and Tamperproof (neat 1 )

proxy between subjects and objects. It takes authorization decisions upon the policy.

1 http://www.ois.com/Products/MILS-Technical-Primer.html

SR(S, R) ∧ P RA(R, A, O) ⇒ Access(S, A, O) U RA(U, R) ∧ P RA(R, A, O) ⇒ Static(U, A, O) SU (S, U ) ∧ Access(S, A, O) ⇒ Dynamic(U, A, O)
Table 2 Rules for fundamental triples in Rbac.

Denition 5 Fundamental triples. The three following fundamental triples symbols must appear in the intensive database idb, and the set of rules P must dene how to derive the corresponding relations Access ⊆ Subject × Action × Object, Static ⊆ U ser × Action × Object and Dynamic ⊆ U ser × Action × Object.

The relation Access is the set of ac permissions granted to subjects. Static is the set of permissions granted to users independently of the subjects they use. Dynamic is the set of permissions granted to users through the subjects. The inclusion Dynamic ⊆ Static must hold in any model.

Authorizations decisions are based upon triples Access derived from the state.

Thus, the reference monitor can be modelled as a function:

F : Subject × Action × Object → {f alse, true} F(s, a, o) = true if (s, a, o) ∈ Access f alse otherwise
The three rules showed in table 2 dene the triples in the Rbac model. According to the sample toy state of table 1, user Bob is assigned to two roles r 1 and r 3 . One may be interested by the authorizations statically granted to Bob which is {(r, file 1 ), (r, file 2 ), (r, file 3 ), (w, file 2 ), (r, file 4 ), (w, file 4 ), (x, file 4 )} by means of the query:

{(a, o) | Static(Bob, a, o)} 2.2.2

ac models hierarchies

The Rbac standard contains two major features to make ac administration easier:

role hierarchies and constraints. Hierarchies are a way to reduce redundant user and permission-role assignments. Roles are given a preorder (reexive, transitive) modelling an is a relationship. Relation r 1 r 2 means that every permissions granted to role r 1 are granted to r 2 and that each user who is a member of role r 2 is also a member of r 1 . Our framework generalizes this approach and takes recommendations of [START_REF] Li | A critique of the ANSI standard on rolebased access control[END_REF] If dened, a Senior S relation should be used in the denition of ac triples. For instance, in the Rbac models with role hierarchies, the rule deriving the Access relation is redened as follows, in order to take the role hierarchy into account:

SR(S, R) ∧ Senior R (R, R ) ∧ P RA(R , A, O) ⇒ Access(S, A, O)
State from table 1 is an instance of the at Rbac model, without role hierarchy.

Assume that we add r 5 into roles and that r 5 inherits r 4 Senior Role (r 5 , r 1 ). With the extended Access rule, any user who is assigned to r 5 has at least r access on file1, file2 and file3 because these permissions are granted to r 1 .

Mutual exclusion relation

Another important feature introduced in the ac literature is mutual exclusion, which is the main constraint dened in the Rbac standard [START_REF] Ferraiolo | Role-Based Access Control[END_REF]. For instance, one may dene that no user can be assigned to both roles r 3 and r 4 , because they stands for mutually incompatible roles.

As it is the case for hierarchies, mutual exclusion needs two relations: an extensive one SoDD and an intensive one SoD which is its symmetric closure. Moreover, when both an exclusion and an inheritance relation have been dened on the same sort, an additional rule must be dened in P , to ensure that exclusion is propagated via inheritance (Gavrila and [START_REF] Serban | Formal specication for role based access control user/role and role/role relationship management[END_REF]. Last denition is still incomplete: we have not dened which constraint the mutual exclusion relation really enforces. We have neither expressed that an inheritance relation should be antisymmetric nor that a subject should be assigned to a unique user.

As a matter of fact, we have only expressed how to dene the policy I . We will show in the next section how to dene the conditions upon which the policies are consistent according to a set of constraints.

For instance, in the toy Rbac state of table 1, one states that r 3 and r 4 are mutually exclusive by adding SoD Role (r 3 , r 4 ) into the state. It may be a way to ensure that request (allowed to r 3 ) and approval (allowed to r 4 ) of major expenditure are done by two separate people. In the toy Rbac state, it should be inconsitent to state SoD Role (r 1 , r 3 ) because user Bob is assigned to both.

Framework summary

Policies are logical models (in the model-theoretic sense) of a theory dened by an ac model. The word model is indeed prone to confusion. We use the term (ac) model to refer to the structure that describes how rights are organized and granted (i.e., the meaning of model in the ac literature). We explicitly use the term logical model to refer to a model-theoretic interpretation which satises a set of closed Fol formulae. This preliminary modelling step is paramount for addressing further issues. The proposed framework is closely related to the deductive database paradigm. In this paradgim, a database is dened with a schema (i.e., the ac vocabulary V oc) and a set of deduction rules (i.e., expressed in Datalog).

An ac state is considered as a set of relational data structured accordingly to a given vocabulary. A policy is a set of facts derived from a state and a set of rules.

Formally, we have dened an ac model as a pair AC = (V oc, P ) composed as follows:

V oc, the access control vocabulary : a set of unary relations called sorts and n-ary relations between these sorts. This vocabulary sets the core of the ac model used to organize the policies. An intepretation I of edb is a state. P : a set of Datalog C rules dening the ac model rules. These rules allow deducing consequent facts from I, thus dening an intensive vocabulary idb and a policy I over idb.

One of our main objectives is to treat constraints as rst class citizens. In the next section, we will extend the denition of (simple) ac model to be a triple AC = (V oc, P, Σ). This renement includes a set Σ of Fol formulae modelling the ac model constraints. They are expressed by data dependencies, which subsume the expressive power of traditional deductive database such as Datalog C . As shown in this paper, this enhanced expressivity is needed to model complex integrity constraints found in ac models. Whereas formulae of P allow deducing the policy from a given state, those from Σ restrict I and I . The denition and usage of Σ are dened in the next section.

3 Access Control Constraints

Among the formal tools available in the database area, data dependencies (a.k.a integrity constraints ) have been dened to capture integrity requirements on relational data. In a unication attempt, they have been dened as Fol sentences (Abiteboul et al., 1995, Chapter 10). In the proposed framework, dependencies are used to capture ac constraints: they capture formal integrity requirements of policies.

Data dependencies

Dependencies share common characteristics with Datalog deduction rules, but they form a larger subclass of Fol sentences. Data dependencies are categorized into classes of increasing expressivity. The best known classes are functional (fd), inclusion (ind)

and multivalued (mvd) dependencies [START_REF] Abiteboul | Foundations of Databases[END_REF]. Expressive classes have been developed to express complex statements on relational data. They can model semantic relationships in spatial, temporal or multimedia databases.

One of the most general form of dependencies is constrained tuple-generating dependencies (ctgd) [START_REF] Michael | Chasing constrained tuple-generating dependencies[END_REF] which are Fol sentences having the following syntax (we reuse convention from section 2.2):

∀ X R 1 (X 1 ) ∧ . . . ∧ Rn(Xn) ∧ ψ( X) ⇒ ∃ Z Q 1 (Y 1 ) ∧ . . . ∧ Qm(Ym) ∧ φ( Ỹ )
where Z does not designate the whole set of variables in the head but only those which are not already bound by a universal quantier ( Z = Ỹ -X).

Special forms of dependencies considered in this paper are restriction of ctgd:

1. Constraint-Generating Dependencies (cgd), head is restricted to constraints:

∀ X R 1 (X 1 ) ∧ . . . ∧ Rn(Xn) ∧ ψ( X) ⇒ φ( X)
2. Nullity-Generating Dependencies (ngd), head is empty 2 :

∀ X R 1 (X 1 ) ∧ . . . ∧ Rn(Xn) ∧ φ( X) ⇒⊥
3. Full Tuple-Generating Dependencies or Total Tuple-Generating Dependencies (Fulltgd) do not include existentially quantied variables:

∀ X R 1 (X 1 ) ∧ . . . ∧ Rn(Xn) ⇒ Q 1 (X 1 ) ∧ . . . ∧ Qm(X m )
4. Tuple-Generating Dependencies (tgd) or Generalized Dependencies, generalize both ftgd and ind but do not allow constraints:

∀ X R 1 (X 1 ) ∧ . . . ∧ Rn(Xn) ⇒ ∃ Z Q 1 (Y 1 ) ∧ . . . ∧ Qm(Ym)
Dependencies are used either to restrict authorized values in a policy when their heads do not include atoms (e.g., cgd, ngd), or to impose presence of tuples if some other ones are already present in the policy (e.g., ind, mvd, tgd). Note that ngd allow the expression of negative requirements as φ ⇒⊥ is logically equivalent to ¬φ.

In our framework, the set of constraints over an ac model is denoted as Σ. It captures conditions that must hold in the policy. The expressivity of dependencies is needed to capture desirable properties which cannot be expressed in P , which relies on the Datalog C fragment, mainly due to the absence of existential quantier. From the logical perspective the P ∪ Σ of rules and constraints is a logical theory, i.e., a set of closed Fol formulae.

Denition 8 Access control model. An access control model is a triple AC = (V oc, P, Σ),

where Σ is a set of constraints expressed as data dependencies.

The semantics of constraints is given by the standard Fol model-theoretic interpretation of dependencies. An access control policy I built from a state I is consistent i I |= Σ.

The next subsections describe how dependencies are used to express various security requirements of models in an homogeneous way: integrity of states, algebraic properties, semantics of mutual exclusion, constraints on authorizations and administrative prerequisites.

2 ⊥ stands for a logical antilogy (e.g., 0 = 1)

SR(S, R) ⇒ ∃U SU (S, U ) SU (S, U ) ∧ SU (S, U ) ⇒ U = U SU (S, U ) ∧ SR(S, R) ⇒ U RA(U, R)

Integrity constraints on ac states

We dene a category of constraints ensuring that relations are well-founded. For example, whenever a relation over sorts exists, the sorts must exist too. Thus, the sentence U RA(U, R) ⇒ U ser(U ) ∧ Role(R) should be enforced in any Rbac policies: a role can be assigned to a user only if both the user and the role exist. This can be considered as an equivalent to foreign key constraints in rdbms. These kinds of constraints ensure that what is actually stored is consistent. This leads to the denition of well-founded state.

Denition 9 Well-founded state. Let Λ be a set of constraints Λ ⊆ Σ involving only symbols of the extensive database edb, such that for each n-ary relation R ∈ edb over sorts S 1 . . . Sn ∈ edb, Λ contains an inclusion dependency of the form: R(ID 1 , . . . , IDn) ⇒ S 1 (ID 1 ) ∧ . . . ∧ Sn(IDn)

Let I be a state. Then I is well-founded if I |= Λ.

For instance, in the Rbac standard it is dened that each subject has to be assigned to a unique user and that a role can be used by a subject only if the role is assigned to the user who owns the subject. These constraints can be dened by dependencies as shown in table 3. These requirements are satised by the Rbac state given in table 1, thus this state is a well-founded one.

The dependencies paradigm allows the formalization of the next suggestion found in the critique of the Rbac standard [START_REF] Li | A critique of the ANSI standard on rolebased access control[END_REF]:

Suggestion 2: The standard should accommodate Rbac systems that allow only one role to be activated in a session This constraints can be captured in a straightforward way by means of a functional dependency that enforces a key constraint SR(U, R) ∧ SR(U, R ) ⇒ R = R . Actually, this requirement is not satised by table 1, because Alice endorses two dierent roles in session S1.

Algebraic constraints of relations

ac models hierarchies are commonly dened as partial orders for avoiding cycles (e.g., [START_REF] Kuhn | Mutual exclusion of roles as a means of implementing separation of duty in role-based access control systems[END_REF] for Rbac or [START_REF] Miège | Dénition d'un environnement formel d'expression de politiques de sécurité : modèle Or-BAC et extensions[END_REF] for Orbac). Moreover, a mutual exclusion is dened as irreexive to prevent a sort from being mutually exclusive with itself (e.g., [START_REF] Li | On mutually-exclusive roles and separation of duty[END_REF]). As example, antisymmetry of inheritance relation and irreexivity of mutual exclusion in Rbac can be expressed by dependencies, as given in table 4.

Moreover, some additional properties may be desirable. For example some models (e.g., Lattice-Bac [START_REF] Sandhu | Lattice-based access control models[END_REF])) organize sorts using forests of trees, forests of inverted trees or lattices (posets in which any two elements have a join and a meet).

These additional requirements over Senior S and SeniorD S relations can be expressed by cgd. Note that the restriction of a hierarchy to a lattice could not be expressed in Datalog-based framework, because these frameworks lacks existentially quantied variables, and the property states that there exists some meet and join for any given pair of elements.

Semantics of mutual exclusion

Although the intensive SoD S ∈ idb relation ensures that there is a mutual exclusion on sort S, the principles of mutual exclusion can be applied from dierent perspectives. In the Rbac model, if two roles r and r are stated as mutually exclusive, several interpretations can exist [START_REF] Crampton | Specifying and enforcing constraints in role-based access control[END_REF]. All these dierent semantics can be stated respectively by means of cgd: no user could be assigned to both roles r and r :

SoD Role (R, R ) ∧ U RA(U, R) ∧ U RA(U, R ) ⇒ ⊥
no subject could be assigned to both r and r :

SoD Role (R, R ) ∧ SR(S, R) ∧ SR(S, R ) ⇒ ⊥
no common permission could be granted to both r and r : SoD Role (R, R) ∧ P RA(R, A, O) ∧ P RA(R , A, O) ⇒ ⊥ no action over a common object could be granted to both r and r :

SoD Role (R, R ) ∧ P RA(R, A, O) ∧ P RA(R , A , O) ⇒ ⊥
For instance, according to the rst semantics, it is inconsistent to add SoD Role (r 1 , r 2 ) in the state given in table 4, because Alice is granted both roles r 1 and r 2 . According to the second semantics, there is an inconsistency because of session S1. However, according to the third semantics, there is no inconsistency because no permission is granted to two dierent roles.

Senior Role (R, R ) ∧ Senior Role (R , R) ⇒ R = R SoD Role (R, R) ⇒ ⊥

Access(S, A, O)

⇒ ∃R SR(S, R)

∧ P RA(R, A, O) Static(U, A, O) ⇒ ∃R U RA(U, R) ∧ P RA(R, A, O) Dynamic(U, A, O) ⇒ ∃S SU (S, U ) ∧ Access(S, A, O)
Table 5 Constraints on authorizations in Rbac.

Constraints on authorization relations

The Rbac model imposes that any authorization must be granted via a role [START_REF] Ferraiolo | Role-Based Access Control[END_REF]:

Property 3.2: A subject s can perform an operation op on object o only if there exists a role r that is included in the subject's active role set and there exists an permission that is assigned to r such that the permission authorizes the performance of op on o.

This property can be considered as fundamental in structured ac models. Dening intermediate sorts between users and permissions is a way to simplify administration tasks. Bypassing these sorts is error-prone and may lead to ambiguities within policies.

Thus, we argue that such a property dened for Rbac should be generalized. According to the rules for triples given in table 2, the constraints of table 5 can be derived. These tgd use existentially quantied variables shared among multiple predicates. Such sentences can not be expressed in Datalog-based frameworks because they lack the existential quantier. This quantier is needed to capture so called invented values in the database terminology, i.e., unknown values that have to be present in a policy to ensure its consistency.

Administrative prerequisite

An administrative prerequisite enforces the presence of tuples before allowing administrative operations [START_REF] Ferraiolo | Role-Based Access Control[END_REF]. Administrative operations consist in updates, insertions and deletions of tuples within the state I. If any administrative prerequisite, expressed by some dependencies, is violated, the transaction initiated by the administrator will not be committed.

∀ X R(X R ) ∧ . . . ∧ Required R (X) ∧ φ( X) ⇒ ∃ Z R(X R ) ∧ . . . ∧ ψ( Ỹ )
For instance, in the Rbac models, administrative prerequisites are used for preventing administrators from assigning roles to users if some other role has not already been dened. This is an example of a prerequisite over the relation U RA. The following sentences express these statements. Dening RequiredD(r 1 , r 2 ) in I imposes that whenever a user is assigned to r 2 , then there must be at least one user assigned to r 2 .

RequiredD(R, R ), Required(R , R ) ⇒ Required(R, R ) U RA(U, R), Required(R, R ) ⇒ ∃U U RA(U , R )

Constraint verication

From now on, we have dened the three basic components of an ac model. The task of dening the vocabulary V oc (the names of subjects, roles, assignments, etc.), the set of administrative rules P and the set of integrity constraints Σ is dedicated to the ac model designer. Administrators dene only the state I, as I = P (I) is computed from I and P . The policy is consistent if I |= Σ. Thus, from a logical perspective, there are only a few dierences between P and Σ which can be considered as a whole as a logical theory T = P ∪ Σ.

Formal characterization

The main dierence between P and Σ lays in their usage: rules are used for computing the policy from the state, whereas constraints are used to impose restrictions on authorized instances of I . Notice that the uniqueness and computability of I is ensured by the properties of the fragment of Fol used for P .

In this section we rely on two theoretical problems over logical theories:

the satisfaction problem. Answering whether a policy I satises a given Fol sentence σ: I |= σ. This problem is central for computing I from I, for answering queries and for checking whether a policy satises the set of constraints for a given model. The satisfaction problem is decidable for the class of formulae used for AC = (V oc, P, Σ).

the logical implication problem. Answering whether a set of closed formulae T logically implies a closed formula σ: T |= σ or, in other words, deciding if any policy model of a theory T is also a model of the single sentence σ. This problem is central for simplifying logical theory or for checking model consistency from an abstract perspective, without considering any state. This problem is decidable in the class of ftgd extended with constraints. However, it is semi-decidable (it may not halt for negative answers but will always halt for positive ones) for larger classes of dependencies such as ctgd.

As dependencies such as ctgd are strictly more expressive than Datalog C , and as they share the same Fol semantics, we will actually treat the sentences of P as dependencies to build and homogeneous logical theory T made of rules and constraints.Thus, it is possible to use the same proof procedures for both rules and constraints without distinction.

We have implemented the proof procedures for dependencies presented in [START_REF] Beeri | A proof procedure for data dependencies[END_REF], [START_REF] Michael | Chasing constrained tuple-generating dependencies[END_REF] and [START_REF] Coulondre | A top-down proof procedure for generalized data dependencies[END_REF] to validate our approach. As shown in section 4.6, our prototype allows automatizing the consistency checking of Rbac policies and furnishing proof of previous results independently proposed [START_REF] Serban | Formal specication for role based access control user/role and role/role relationship management[END_REF].

Administrative review

One of the features expected from an access control model implementation is the administrative review. This set of operations has been dened in the Rbac standard:

When U RA and P RA relation have been created, it should be possible to view the contents of those relations from both the user and role perspectives [. . . ]. In the present framework, administrative reviews are simple conjunctive queries over I . Therefore, the requirements of the standard denition are met.

Denition 13 Administrative reviews. Any conjunctive query (from the standard database sense) built upon the vocabulary V oc is an administrative review.

Examples of queries built upon the Rbac model vocabulary V oc are respectively

(1) the set of permissions granted directly (without hierarchy) to users through their roles , (2) the set of users who can execute an object, whatever it is, (3) the set of users who are assigned the role r 1 :

1. {(u, a, o) | ∃r U RA(u, r) ∧ P RA(r, a, o)}, 2. {u | ∃s, o, r SU (s, r) ∧ SR(s, r) ∧ SeniorD(r, r ) ∧ P RA(r , x, o)} 3. {u | U RA(u, r 1 )}
The answer to the last query, on the state given in table 1, is {Alice, Bob, Charly}. When I only is queried, we can rely upon any rdbms to provide the querying mechanism, as the state is stored in extension in relational tables. The technical diculty is to compute and to query the policy I . As far as Datalog or Datalog C is chosen, I can be computed quite eciently. This computation is still valid as long as I is not modied, thus allowing some caching optimizations techniques. We suggest four approaches to compute the policy I from a state I and rules P : use recursive queries and advanced features provided by common rdbms. For instance, Microsoft sql-Server oers the Common Table Expression system which allows (restricted) recursive queries. From the logical point of view, this kind of feature can be seen as restrictions of Datalog (e.g., set-based operations are not provided), use triggers and stored procedures to compute I on the y on each modication of I. This approach can be implemented for simple access control models (when cardinality of T is small enough), but will become hard to maintain if many roles are dened. Indeed it is needed to code specic procedures for each Fol sentence in P . use a deductive database engine. Several ecient engines have been developed, for instance dlv 3 or xsb 4 . They can compute I and include recursive queries and simple forms of dependencies. However, expressive dependencies such as tgd are not handled. develop an external inference engine out of an existing rdbms while relying on the mechanisms from the rdbms for access and modication of state. As basic operations are common to both computation of I and logical inference over T (see next section), we have implemented this approach in a library dedicated to expression and inference of general classes of dependencies.

Policy completeness and consistency

The validity of an ac policy is checked by verifying, given a model AC = (V oc, P, Σ), whether I |= Σ. Unsatisfaction of a set of constraints by a policy can fall into two categories:

the policy is inconsistent : some cgd or ngd are not satised. For instance, a policy is said to be inconsistent if antisymmetry, irreexivity or exclusion relations are not satised, the instance is incomplete : some tgd are not satised. For instance, a policy is said to be incomplete if some properties of authorization relations or administrative prerequisites are not satised.

If a policy is inconsistent or incomplete, administrators have to correct the state. Whenever a policy is inconsistent, deletion of existing facts or value updates should be favored. Whenever a policy is incomplete, addition of facts should be privileged.

Examples of possibles corrections of inconsistent or incomplete policies are given in table 6. Several ac models have introduced dynamic sorts. For instance, in the Rbac family, the unique dynamic sort is subject, the other ones (role, user, action, object, permission ) are static, as well as relations between them (e.g., user-role assignment U RA, permissionrole assignment P RA). This specialization can be expressed according to the rights granted to administrators over the state. Sorts and relations in edb can be categorized as follows:

static: only administrators can modify this part of the state. Static aspects are stable according to the execution of the system and do not depend on the end-user activity.

dynamic: administrators are not the only ones having the right to modify this part of the state. For instance, the sort of Subject in Rbac acts on behalf of an user. A SU is created each time a user logged into the system. In ac models involving time or space, these sorts and relations are out of the sovereignty of the administrators.

It is straightforward to dene static comparison of policies from the relational paradigm. In section 2.2.1, we have dened three fundamental authorization triples, i.e., Access, Dynamic and Static. Considering the last one, we can compare static restriction of policies by comparing the sets of tuples in Static.

Denition 14 Static comparison of policies. Let be I 1 and I 2 two consistent and complete policies, expressed on two dierent ac models AC 1 et AC 2 .

Let Static 1 be the set of static authorization triples of I 1 , and Static 2 be the set of static authorization triples of

I 2 . Static 1 ∈ I 1 ⊇ I 1 et Static 2 ∈ I 2 ⊇ I 2 .
The policy I 1 is as or more more restrictive than I 2 i:

Static 1 ⊆ Static 2
The policy I 1 is as or more more permissive than I 2 i:

Static 1 ⊇ Static 2
The policies I 1 and I 2 are equivalent i:

Static 1 ⊆ Static 2 and Static 1 ⊇ Static 2
Actually, static sorts constitute the backbone of ac models. For instance, roles in Rbac, labels in Mac, organizations in Orbac or tasks in Trbac are static sorts.

Thus, it is worth verifying static enforcement of ac policies, as this can ensure that most robust properties are valid in any state of the policies [START_REF] Li | On mutually-exclusive roles and separation of duty[END_REF].

Model properties

Whereas previous subsections have been devoted to policy checking, this section considers ac models from an abstract perspective, without reference to any particular policy or state. The main problem we address is logical implication, in particular for model simplication purposes. For example, in the case of a new tailored ac model, where many collaborative designers from dierent sites might be involved, the associated logical theory may become quite large (e.g., hundreds of rules and statements).

Thus, for practical purposes, it is necessary to reduce the size of the theory.

Denition 15 Redundancy in an ac model. Let be T = P ∪ Σ the logical theory of an ac model made of rules and constraints. Let be σ ∈ T , if T \{σ} |= σ then the dependency σ is said redundant, moreover T \{σ} and T have the same models.

The authors of [START_REF] Michael | Chasing constrained tuple-generating dependencies[END_REF] give two bottom-up (also known as forward) chase procedures for solving the implication problem of ctgd: given a set of ctgd Σ, and a single ctgd σ (of the form φ ⇒ ψ), determine whether in every policy where Σ is satised, σ is also satised. If the chase procedures successfully stop, then Σ logically implies σ, stated briey as Σ |= σ.

The operational nature of proof procedures for ctgd is based on the concept of tuple (a grounded atom, with no variables). The procedures saturates a symbolic database made of tuples by repeated applications of dependencies, to produce a model of the set of dependencies. In a precise sense, this model is the most general possible one, it is a canonical universal one [START_REF] Calì | Taming the innite chase: Query answering under expressive relational constraints[END_REF].

Maher and Srivastava's procedures keep the same strategy as the original chase of [START_REF] Beeri | A proof procedure for data dependencies[END_REF] extended to deal with constraints. For sake of clarity, original algorithm is given on page 29. Its design is the core of other procedures for dependencies and it is conceptually simpler to understand. It's theoretical complexity has been shown to be exponential [START_REF] Beeri | A proof procedure for data dependencies[END_REF]. The very basic outline of the chase is as follows, input is a set of dependencies Σ and a single dependency σ:

1. initialization : the chase picks a valuation µ to hypothesize the existence of some tuples so that the body φ of σ is satised, 2. main loop: treats Σ as a closure operator generating tuples Σ(φ), that is repeatedly applies dependencies from Σ to produce new facts, 3. exit condition : at the end of each loop, the following conditions are checked and three termination cases are possible:

(a) if Σ(φ) contains an inconsistency, return Σ |= σ vacuously, (b) if Σ(φ) contains an instance of ψ, that is there is a valuation ν that extends µ such that ν(ψ) ∈ Σ(φ), return Σ |= σ, (c) if Σ(φ) neither produces new facts nor contains a instance of ψ, return Σ |= σ.

The ctgd implication problem is semi-decidable: the procedure always halt when the answer is positive, but may run forever if the answer is negative. However, there are some interesting decidability results holding in various subclasses of ctgd such as (Weakly) Guarded-tgd that include existentially quantied variables [START_REF] Calì | Taming the innite chase: Query answering under expressive relational constraints[END_REF]. For example, the chase is decidable for tgd having no existentially quantied variable [START_REF] Beeri | A proof procedure for data dependencies[END_REF].

Sample result

This section illustrates the proposed approach by simplifying integrity properties of mutual exclusion and inheritance dened over a common sort. For this illustation, we use the set of integrity properties for Rbac models dened by [START_REF] Serban | Formal specication for role based access control user/role and role/role relationship management[END_REF]. In the present approach, these properties are modelled by constraints in Σ.

The authors have manually proved that the set of properties in table 7 can be reduced to a smaller set. Using some proof procedures for dependencies, we can simplify their logical theory by eliminating redundancies.

We provide a sample execution trace obtained using a prototype. This prototype, written in C++, can handle the ctgd as well as its subclasses. It relies on an external constraint solver over reals to handle constraints. Three dierent chases have been implemented : [START_REF] Beeri | A proof procedure for data dependencies[END_REF], [START_REF] Michael | Chasing constrained tuple-generating dependencies[END_REF] and [START_REF] Coulondre | A top-down proof procedure for generalized data dependencies[END_REF]. Given a logical formalization of an ac written using dependencies, the prototype With σ 3 (sentence [1], mutual exclusion is symetric), SoD(r 2 , r 1 ) is derived. Next, applying σ 6 (sentence [3], exclusion is propagated through inheritance ) twice, SoD(r 0 , r 2 ) et SoD(r 0 , r 1 ) is derived. Added to tuples: exclusion(_r_0,_r_0); 3; Added to activations: {R:_r_0,R1:_r2_0,R2:_r_0}; 6,2; ...[3] treated Next, using σ 3 (sentence [1]), SoD(r 2 , r 0 ) and SoD(r 1 , r 0 ) are deduced. Thus, by σ 6 (sentence [3]), SoD(r 0 , r 0 ) is derived. -------------------------------------------------------------------------------------there is an inconsistency in the constraint store F|=g vacuously (VACUOUSLY) number of rules applied for closure F(l):7 this chase was :0.088197 seconds long number of tuples generated:10 Finally, applying σ 2 (sentence [2], exclusion is irreexive ), an antilogy is derived. Thus, the chase procedure proved that {σ 2 , σ 3 , σ 6 } |= σ 5 . The prototype can be used to derive other sample theorem from the dependencies of table 7. Let be Σ the six dependencies shown in the table. The chase procedures can prove that Σ\{σ 4 } |= σ 4 , Σ\{σ 5 } |= σ 5 and that Σ\{σ 4 , σ 5 } |= σ 4 , σ 5 . This example illustrates the utility of the proposed framework. Given an ac model AC = (V oc, P, Σ), an automated proof of non-trivial properties can be provided. For instance, besides the above obtained theorems, we have been able to derive the following results: read and write access over an objet in Mandatory Access Control (Mac) are granted to a subject i the subject's clearance level is equal to the object's condentiality level [START_REF] Sandhu | Lattice-based access control models[END_REF], a root role which inherits all other ones cannot exist in an Rbac policy where two roles are mutually exclusive [START_REF] Benantar | Access Control Systems -Security, Identity Management and Trust Models[END_REF], dynamic authorizations are a subset of static authorizations in Rbac policies [START_REF] Ferraiolo | Role-Based Access Control[END_REF].

5 Related work

General comparison

Our work is closely related to [START_REF] Barker | Flexible access control policy specication with constraint logic programming[END_REF] which expresses Rbac models in constraint logic programming, to [START_REF] Halpern | Using rst-order logic to reason about policies[END_REF] which identies a subset of Fol for ac models, to [START_REF] Bertino | A logical framework for reasoning about access control models[END_REF] which describes a C-Datalog framework for representing ac models, to [START_REF] Jajodia | Flexible support for multiple access control policies[END_REF] which denes a exible access control framework, to [START_REF] Li | DATALOG with constraints: A foundation for trust management languages[END_REF] which uses Datalog C and [START_REF] Miège | Dénition d'un environnement formel d'expression de politiques de sécurité : modèle Or-BAC et extensions[END_REF] which uses the Datalog ¬ for dening the Orbac model. Our main goals were to provide a framework for ac which: makes a clear separation between policies and models and has a clear semantics, is expressive enough to capture and generalize roperties of ac models, treats policy constraints as rst-class citizens, provides readable algorithm execution traces for designers and administrators.

The background we have settled in section 2 is based on Datalog C . This logical framework has been often treated as a middle-ground formalism to which many other logical based frameworks can be reduced, for instance in the work of [START_REF] Detreville | a logic-based security language[END_REF][START_REF] Jim | SD3: A trust management system with certied evaluation[END_REF][START_REF] Bertino | A logical framework for reasoning about access control models[END_REF][START_REF] Li | DATALOG with constraints: A foundation for trust management languages[END_REF]. Moreover, Datalog C has shown to be able to capture several ac models, and various extensions of Rbac model [START_REF] Joshi | A generalized temporal role-based access control model[END_REF][START_REF] Maria | GEO-RBAC: A spatially aware rbac[END_REF]. As the present framework subsumes Datalog C , it can basically capture these models.

The main dierence with the above previous work is the fruitful use of data dependencies as a unifying logical framework which encompasses both traditional ac rules and integrity constraints. Thus, constraints are expressed in the very same model, and not expressed in an independent and dierent framework. As constraints are integrity requirements of policies, we argue that integrating them in the model as soon and as tightly as possible is a step towards ensuring ac robustness.

We rely on some known results for data dependencies, in order to provide wellfounded tools for reasoning on policies. An interesting feature of these proof procedures is that they do not require any prior translation of Fol formulae of rules P and integrity constraints Σ (e.g., by means of Skolemization or rewriting rules). This property leads to native clear traces of automated proofs, as given in section 4.6. This greatly enhances the readability of inference results for design and maintenance purposes. Finally, by means of the prototype, we have been able to re-prove in an automated way some interesting results found in the literature.

5.2 Frameworks built upon Datalog [START_REF] Bertino | A logical framework for reasoning about access control models[END_REF] and [START_REF] Li | DATALOG with constraints: A foundation for trust management languages[END_REF] have used the Datalog framework, respectively C-Datalog which allows object-oriented denitions, and Datalog C which includes constraints. These frameworks are able to capture extended Rbac models such as Temporal-Rbac [START_REF] Bertino | TRBAC: A temporal role-based access control model[END_REF]. The basic components of the present proposition (sections 2 and 2.2) reuse and extend some of their formal models. (Li et al., 2003), [START_REF] Jim | SD3: A trust management system with certied evaluation[END_REF][START_REF] Detreville | a logic-based security language[END_REF] have extended Datalog with specic constructions which are reduced into standard Datalog formulae. However, we have not used rewriting procedures which may cloud the debugging steps and puzzle administrators.

5.3 Other frameworks built upon logic [START_REF] Jajodia | Flexible support for multiple access control policies[END_REF], [START_REF] Barker | Flexible access control policy specication with constraint logic programming[END_REF] and [START_REF] Halpern | Using rst-order logic to reason about policies[END_REF] describe logical programs able to express general ac models. These propositions address the problems arising with the use of closed policies (in which access is by default denied and authorizations are only positive), open policies (access is granted by default)

or hybrid policies (authorizations and denial can be both explicitly dened). [START_REF] Miège | Dénition d'un environnement formel d'expression de politiques de sécurité : modèle Or-BAC et extensions[END_REF] use Datalog ¬ to deal with negative authorization (prohibition). These logical frameworks allow a permissive use of negation in formal sentences, whereas we chose to favor existential quantiers. However, our framework is able to support a restrictive use of negation by means of ngd for instance. Our framework captures complex integrity requirements considered as fundamental in Rbac, which are not expressible in other ones. Moreover, we provide an eective procedure to automatize administrative operations.

Our framework is tightly linked to the database area and makes a clear distinction between policies and models. This separation, advocated by [START_REF] Li | A critique of the ANSI standard on rolebased access control[END_REF], is not explicit in the work of [START_REF] Barker | Flexible access control policy specication with constraint logic programming[END_REF] and [START_REF] Halpern | Using rst-order logic to reason about policies[END_REF], as well as in the logic programming paradigm on a more general point of view. Finally, we have reused and extended some denitions of [START_REF] Ferraiolo | Role-Based Access Control[END_REF] (properties of Rbac) and results of (Gavrila and Barkley, 1998) (consistency of Rbac databases)

which were not integrated into other frameworks.

Access control constraints

Constraints have received much attention in ac models. Rbac is argueably one of their most prominent representatives for which many kinds of constraints have been proposed [START_REF] Gligor | On the formal denition of separation-of-duty policies and their composition[END_REF][START_REF] Ahn | The RSL99 language for role-based separation of duty constraints[END_REF][START_REF] Crampton | Specifying and enforcing constraints in role-based access control[END_REF]. These suggestions either dene and categorize new kinds of constraints (e.g., the variations on mutual exclusion outlined in section 3.4) or proposed specication languages for constraints. Most of these constraints are dened as a way to enforce separation of duties, and are variants of mutual exclusion.

The algebra of [START_REF] Li | Beyond separation of duty: An algebra for specifying high-level security policies[END_REF] for specifying constraints encompasses these approaches but consider constraints as high-level organization requirements. Our approach is quite dierent, in the sense that constraints are dened closer to the model at a lower level. Thus, we can capture intrinsic properties (e.g., constraints on authorization triples, prerequisites) as well as general integrity requirements (e.g., states well-foundedness, algebraic properties of relations) which are usually taken into account separately.

Discussion

This section discusses the main choices we made. We divide this section into the ac structure design choices and the Fol fragment choice.

Design and administration

By drawing a distinction between an ac model and an ac policy instanciated from a model, we can dene two ac-related activities:

model design is the task of dening the ac model. The model designer sets up the sorts and relations of the model (V oc), its rules (P ) and the properties that must be enforced (Σ). For instance, a model designer may dene that tasks and roles are used to structure policies. As an analogy in the database eld, the model designer counterpart is the database administrator, who denes tables (V oc), views (P ) and keys between tables (Σ).

policy administration is the task of dening the state I. The policy administrator sets up the facts of an ac model instance, but can not dene I directly because it is automatically derived from I using P . According to the above example, a policy administrator sets that physician and surgeon are roles, and is responsible for assigning these roles to individuals. As an analogy in the database eld, the policy administrator counterpart is an end-user, whose job is to query and modify the policy, but who is not able to modify the schema.

Model structure

In section 2, we introduced the structure of AC = (V oc, P, Σ) made of three components and we dened the major design choices we have made:

ac models are dened as logical theories while being narrowed to decidable fragments without negation, disjunction nor function symbols in P , the vocabulary is partitioned into sorts and relations in a many-sorted Fol paradigm, rules (P ) and constraints (Σ) are distinguished, the dierence between a state I and a policy I is logically made explicit.

One may argue that these choices are somewhat restrictive. The administrator's tasks are limited to extensive policies management, i.e., to tuple management in the ac state. It might be possible to allow them to expressed their own formulae in P or Σ.

However, we think this is not desirable, as this would blur the responsabilities between designers and maintainers and would introduce higher policy checking complexity. In such an approach, the stability of the ac models would not be guaranteed through the policies lifetime, in particular consistency and interoperability of updated models.

Fragments of logic for access control

The logical fragment of Fol we used to dene P and Σ is quite restrictive: negation, disjunction and function symbols are not allowed. The main argument is that we obtain a unique and computable model of P . Computability is necessary because the reference monitor has to answer each access request. Uniqueness for integrity checking purposes is required, in order to avoid checking the satisfaction of Σ over multiple models of P . Moreover, uniqueness may ease the understanding of intensive policies by administrators.

Furthermore, we chose to have a more expressive framework for constraints than for rules, by favoring existential quantication over negation. The main goal is to be able to model some of the most important constraints commonly identied for ac models, which cannot be expressed in Datalog models. Even with a quite simple ac model (for instance, with a few sorts, relations and principles), most of the properties given in section 3 require existentially quantied variables (e.g., sessions integrity properties, restricted hierarchies, authorizations properties and administrative prerequisites).

Conclusions and perspectives

In this paper, we presented a logical framework AC = (V oc, P, Σ) for ac models, which relies on three abstract components. The key idea is to express and handle ac models, policies and constraints in an homogeneous way within the very same logic background by means of database integrity theory (not to deploy ac policies in databases). We then showed how to use well-founded procedures in order to enforce and check constraints, and to provide a formal trace of inferences. The proposed framework is not universal because of the choice we made to focus on access control constraints and to treat them as rst-class citizens. It however allows for expressing several classical models and extensions found in the literature. It also takes into account some major recommendations that had been previously addressed to Rbac models. Moreover, the expressivity of general classes of dependencies allows capturing most of the ac model properties considered as fundamental.

We envision several extensions and perspectives: extension of the Fol subclasses, to capture new properties of models. However, algorithms decidablity and tractability should be taken into account. As an example, it may be interesting to use some decidable subclass of tgd by imposing some restrictions on existentially quantied variables, as it is the case for negation in stratied-Datalog for instance, explore automated maintenance of databases [START_REF] Chomicki | Minimal-change integrity maintenance using tuple deletions[END_REF], and data integration [START_REF] Fagin | Inverting schema mappings[END_REF] to x non-consistent policies. Data integration may be a fruitful perspective for policies creation expressed in dierent models [START_REF] Li | Access control policy combining: theory meets practice[END_REF], broadening the scope of policies. Indeed, it would be valuable to model administrative policies, which dene administrator rights over ac policies. This could be useful for instance when a huge policy requires several administrators, each of them being allowed to handle only a part of the policy.

another emerging topic is usage control and privacy protection. The basic components and denitions we presented can be used to dene next generation ac models and policies, as it has been done with Rbac models [START_REF] Ni | Privacy-aware RBAC -leveraging RBAC for privacy[END_REF].

  into account: Suggestion 4: The Reference Model should maintain a relation that contains the role dominance relationships that have been explicitly added, and update this relation when the role hierarchy changes. For any sort S ∈ edb of an ac model, we dene two relations: a dominance relation SeniorD S ∈ edb stored in the state, and an inheritance relation Senior S ∈ idb dened as the reexive transitive closure of SeniorD S . Please note that we use sux D to distinguish between extensive and intensive predicate. Denition 6 Inheritance. A sort S ∈ edb of an ac model is given an inheritance relationship if a dominance relation SeniorD S with SeniorD S ⊆ S × S is dened in edb and if the following three rules are dened in P : SeniorD S (S, S ) ⇒ Senior S (S, S ) SeniorD S (S, S ) ∧ Senior S (S , S ) ⇒ Senior S (S, S ) S(ID) ⇒ SeniorD S (ID, ID)

Denition 7

 7 Mutual exclusion. A sort S ∈ edb is given a mutual exclusion relationship if a core separation relation SoDD C ⊆ S × S is dened in edb and if a relation SoD S ⊆ S × S is dened with the following two principles in the set of rules P : SoDD S (S, S ) ⇒ SoD S (S, S ) SoD S (S, S ) ⇒ SoD S (S , S) If an inheritance relation Senior S is also set on a sort S, then the following rule must be dened: SoD S (S, S ) ∧ Senior S (S , S) ⇒ SoD S (S, S )

  Denition 10 Restricted hierarchies. Let Senior S ∈ idb be an intensive inheritance relation computed from an extensive one SeniorD S ∈ edb. Senior S is called a limited hierarchy of type: forest of trees, if Σ contains the following fd: SeniorD S (S, S ), SeniorD S (S, S ) ⇒ S = S forest of inverted trees, if Σ contains the following fd: SeniorD S (S , S), SeniorD S (S , S) ⇒ S = S lattice, if Σ contains the following ftgd: S(S ), S(S ) ⇒ ∃S ⊥ Senior S (S , S ⊥ ), Senior S (S , S ⊥ ) S(S ), S(S ) ⇒ ∃S Senior S (S , S ), Senior S (S , S )

  ... '(for all)[R1,R2] SoD(R1,R2)->SoD(R2,R1).' Added to tuples: SoD(_r2_0,_r_0); 1; Added to activations: {R1:_r_0,R2:_r2_0}; 4; Added to tuples: SoD(_r1_0,_r_0); 1; Added to activations: {R1:_r_0,R2:_r1_0}; 5; ...[1] treated Treating [3]... '(for all)[R,R1,R2] SoD(R1,R2),Senior(R,R1)->SoD(R,R2).'

  ... '(for all)[R] SoD(R,R)->Error(reflex) {(1=\=1)}.' Added to tuples: Error(reflex); 2; Added to store: (1=\=1) Added to activations: {R:_r_0}; 8; ...[2] treated -

Table 1 A

 1 sample Rbac state.

					P RA
				Role	Action	Object
	User	U RA	Role	r1 r1	r r	file1 file2
	Alice		r1	r1	r	file3
	Alice		r2	r2	w	file1
	Bob		r1	r3	w	file2
	Bob		r3	r3	r	file4
	Charly		r1	r3	w	file4
	Charly		r4	r3	x	file4
				r4	w	file3
				r4	r	file4
		SR		r4	w	file4
	Subject		Role	r4	x	file4
	S1		r1		SU
	S1		r2	Subject		User
	S2 S3 S4		r1 r3 r4	S1 S2 S3		Alice Bob Bob
				S4		Charly

Table 3

 3 Integrity requirements for SU relation in Rbac.

Table 4

 4 Antisymmetry of role hierarchy, and irreexivity of mutual exclusion.

  Denition 12 Administrative prerequisite. An administrative prerequisite constraint imposes the presence of tuples in I . A transitive prerequisite relation Required R ∈ idb over a relation R is dened as the transitive closure of a relation RequiredD R ∈ edb. Prerequisite constraints can be modelled as (constrained) tgd in Σ by an auxiliary relation RequiredD R of the following form, where the predicate R is present in both the sentence body and head:

Table 6

 6 Examples of inconsistent or incomplete policies corrections 4.4 Static policy comparison

http://www.dbai.tuwien.ac.at/proj/dlv/

http://xsb.sourceforge.net/

If a role inherits another role and that role is in SSD with a third one, then the inheriting role is in SSD with the third one.

Senior(Senior, Role 1 ), SoD(Role 1 , Role 2 ) ⇒ SoD(Senior, Role 2 ).

Table 7 Logical characterization of Rbac constraints (Gavrila and [START_REF] Serban | Formal specication for role based access control user/role and role/role relationship management[END_REF] is used to simplify the model, to compute the policy for a given state, to check the consistency of the policy and to answer administrative queries. Static comparison of policies have not been implemented yet.

The following trace is the result of the execution of the ctgd chase of Maher and Srivastava (1996) implemented in the prototype. Initially, the dependency base is loaded with σ 2 , σ 3 and σ 6 of table 7. The goal is to prove that {σ 2 , σ 3 , σ 6 } |= σ 5 . The following trace is a formal proof of this entailment.

-

[0] SoD(_r1_0,_r2_0); -1; [1] Senior(_r_0,_r1_0); -1; [2] Senior(_r_0,_r2_0); -1; seed : SoD(_r1_0,_r2_0),Senior(_r_0,_r1_0),Senior(_r_0,_r2_0) goal : {(1=\=1) } tgdGoal : (for all)[R,R1,R2] SoD(R1,R2),Senior(R,R1),Senior(R,R2)-> {(1=\=1)}.

Hypothesize three tuples SoD(r 1 , r 2 ), Senior(r 0 , r 1 ) and Senior(r 0 , r 2 ) from the body of σ 5 . Added to tuples: SoD(_r_0,_r2_0); 3; Added to activations: {R:_r_0,R1:_r1_0,R2:_r2_0}; 0,1;

Added to tuples: SoD(_r_0,_r1_0); 3; Added to activations: {R:_r_0,R1:_r2_0,R2:_r1_0}; 3,2; ... Algorithm 1: Chase algorithm from [START_REF] Beeri | A proof procedure for data dependencies[END_REF]