As systems evolve, security administrators need to review and update access control policies. Such updates must be carefully controlled due to the risks associated with erroneous or malicious policy changes. We propose a category-based access control (CBAC) model, called Admin-CBAC , to control administrative actions. Since most of the access control models in use nowadays (including the popular RBAC and ABAC models) are instances of CBAC, from Admin-CBAC , we derive administrative models for RBAC and ABAC, too. We present a graph-based representation of Admin-CBAC policies and a formal operational semantics for administrative actions via graph rewriting. We also discuss implementations of Admin-CBAC exploiting the graph-based representation. Using the formal semantics, we show how properties (such as safety, liveness, and effectiveness of policies) and constraints (such as separation of duties) can be checked, and discuss the impact of policy changes. Although the most interesting properties of policies are generally undecidable in dynamic access control models, we identify particular cases where reachability properties are decidable and can be checked using our operational semantics, generalising previous results for RBAC and ABAC α .

International audience

In the context of multi-user cooperative systems and, in particular, in social networks, personal data is uploaded to user profiles and shared with other users. These data are often jointly owned and associated with different degrees of sensitivity according to the users. Controlling access to such multi-owner data, under the authority of different users, is challenging. Traditional access control policies are not expressive enough to determine whether a data disclosure meets the privacy expectations of the different involved parties. In this work, we propose a fine-grained access control model for multi-user cooperative systems and apply it to the context of social networks. We consider compound objects and extend attribute-based access control with provenance information to specify additional access control constraints. We also present a prototype implementation and provide an experimental evaluation to demonstrate the feasibility of the proposed model.

We present general notions of access control policy composition using the CBAC model. We show that CBAC provides a uniform framework to define compositions of heterogeneous policies (e.g., RBAC and ABAC policies) as required in many practical situations. Compositions can be built both horizontally (where n given policies are combined to define a new policy) and vertically (where policies are extended by adding administration layers). We show that under some conditions on the operations used to build the composition, it is possible to ensure that the result preserves desirable properties (such as liveness and effectiveness). We also discuss mechanisms to detect and eliminate conflicts that may arise when composing policies originating from different sources.

We present a graph-based language for the specification of administrative access control policies in Admin-CBAC, an administrative model for Category-Based Access Control. More precisely, we propose a multi-level graph representation of policies and a graph-rewriting semantics for administrative actions, from which properties (such as safety, liveness and effectiveness of policies) and constraints (such as separation of duties) can be checked using graph traversal algorithms and rewriting properties. Since Admin-CBAC is a generic model, the techniques are directly applicable to a variety of access control models. In particular, we illustrate our techniques for the RBAC and ABAC instances of Admin-CBAC.

We present Admin-CBAC, an administrative model for Category- Based Access Control (CBAC). Since most of the access control models in use nowadays are instances of CBAC, in particular the popular RBAC and ABAC models, from Admin-CBAC we derive administrative models for RBAC and ABAC too. We define Admin- CBAC using Barker's metamodel, and use its axiomatic semantics to derive properties of administrative policies. Using an abstract operational semantics for administrative actions, we show how properties (such as safety, liveness and effectiveness of policies) and constraints (such as separation of duties) can be checked, and discuss the impact of policy changes. Although the most interesting properties of policies are generally undecidable in dynamic access control models, we identify particular cases where reachability based properties are decidable and can be checked using our operational semantics, generalising previous results for RBAC and ABACalpha.

In the context of cooperative systems, data coming from multiple, autonomous, heterogeneous information sources, is processed and fused into new pieces of information that can be further processed by other entities participating in the cooperation. Controlling the access to such evolving and variegated data, often under the authority of different entities, is challenging. In this work, we identify a set of access control requirements for multi-source cooperative systems and propose an attribute-based access control model where provenance information is used to specify access constraints that account for both the evolution of data objects and the process of data fusion. We demonstrate the feasibility of the proposed model by showing how it can be implemented within existing access control mechanisms with minimal changes.

Security-sensitive workflows impose constraints on the controlflow and authorization policies that may lead to unsatisfiable instances. In these cases, it is still possible to find "least bad" executions where costs associated to authorization violations are minimized, solving the so-called Multi-Objective Workflow Satisfiability Problem (MO-WSP). The MO-WSP is inspired by the Valued WSP and its generalization, the Bi-Objective WSP, but our work considers quantitative solutions to the WSP without abstracting control-flow constraints. In this paper, we define variations of the MO-WSP and solve them using bounded model checking and optimization modulo theories solving. We validate our solutions on real-world workflows and show their scalability on synthetic instances.

Administration of access control policies is a difficult task, especially in large organizations. We consider the problem of detecting whether administrative actions can yield in policies where some security goals are compromised. In particular, we are interested in problems generated by modifications --- such as adding/deleting elements to/from the set of possible users or permissions --- of policies specified as term-rewrite systems. We propose to use rewriting techniques to compare the behaviors of the modified version and the original version of the policy. More precisely, we use narrowing to compute counter-examples to the equivalence of rewrite-based policies. We prove that our technique provides a sound and complete way to recursively enumerate the set of counter-examples, even when this set is not finite, or when a mistake of the administrator makes one or both systems non-terminating.

Run-time monitors are crucial to the development of security-aware workflow management systems, which need to mediate access to their resources by enforcing authorization policies and constraints, such as Separation of Duty. In this paper, we introduce a precise technique to synthesize run-time monitors capable of ensuring the successful termination of workflows while enforcing authorization policies and constraints. An extensive experimental evaluation shows the scalability of our technique on the important class of hierarchically specified security-sensitive workflows with several hundreds of tasks.

Access control is a crucial issue for the security of Web Services. Since these are independently designed, implemented, and managed, each with its own access control policy, it is challenging to mediate the access to the information they share. In this context, a particularly difficult case occurs when a service invokes another service to satisfy an initial request, leading to indirect authorization errors. To overcome this problem, we propose a new approach based on a version of ORganization Based Access Control (OrBAC) extended by a delegation graph to keep track of transitive authorization dependencies. We show that Datalog can be used as the specification language of our model. As a byproduct of this, an automated analysis technique for simulating execution scenarios before deployment is proposed. Finally, we show how to implement an enforcement mechanism for our model on top of the XACML architecture. To validate our approach, we present a case study adapted from the literature.

We propose an event-based access control model, called Distributed-DEBAC, that takes into account the behaviour of distributed systems. Distributed-DEBAC policies are specified using an algebraic-functional framework. The declarative nature of the model facilitates the analysis of policies, and direct implementations for access control checking even when resources and information are widely dispersed. We give examples of application.

We propose an access control model that takes into account the specific behaviour of distributed, highly dynamic environments, and describe their representation using an algebraic-functional framework. The declarative nature of the model facilitates the analysis of policies, and direct implementations for access control checking even when resources and information are widely dispersed.

In large, and often distributed, environments, where access control information may be shared across multiple sites, the combination of individual specifications in order to define a coherent access control policy is of fundamental importance. In order to ensure non-ambiguous behaviour, formal languages, often relying on firstorder logic, have been developed for the description of access control policies. We propose in this paper a formalisation of policy composition by means of term rewriting. We show how, in this setting, we are able to express a wide range of policy combinations and reason about them. Modularity properties of rewrite systems can be used to derive the correctness of the global policy, i.e. that every access request has an answer and this answer is unique

The Rewriting Calculus (ρ-calculus, for short) was introduced at the end of the 1990s and fully integrates term-rewriting and λ-calculus. The rewrite rules, acting as elaborated abstractions, their application and the structured results obtained are first class objects of the calculus. The evaluation mechanism, which is a generalisation of beta-reduction, relies strongly on term matching in various theories. In this paper we propose an extension of the ρ-calculus, called ρg-calculus, that handles structures with cycles and sharing rather than simple terms. This is obtained by using recursion constraints in addition to the standard ρ-calculus matching constraints, which leads to a term-graph representation in an equational style. Like in the ρ-calculus, the transformations are performed by explicit application of rewrite rules as first-class entities. The possibility of expressing sharing and cycles allows one to represent and compute over regular infinite entities. We show that the ρg-calculus, under suitable linearity conditions, is confluent. The proof of this result is quite elaborate, due to the non-termination of the system and the fact that ρg-calculus-terms are considered modulo an equational theory. We also show that the ρg-calculus is expressive enough to simulate first-order (equational) left-linear term-graph rewriting and α-calculus with explicit recursion (modelled using a letrec-like construct).