FACPL Tools: Specifying, Analysing and Enforcing Access Control Policies

Contents

Description

The FACPL language is a formal, easy-to-use language that permits specifying access control policies. FACPL is the basis of a feasible and effective approach for defining access control systems. Various applications have been proposed, varying from e-Health to autonomic computing domains.

FACPL is equipped with a powerful Integrated Development Environment (IDE) and a Java library, supporting access control system developers in the tasks of specifying, analysing and enforcing FACPL policies. Figure 1 shows the toolchain enabling the use of the language.


Figure 1. FACPL ToolChain

Developers can use the IDE, in the form of an Eclipse plugin, for specifying the desired policies in FACPL syntax, by taking advantage of the supporting features provided by the environment. The IDE automatically produces a set of Java classes enforcing the FACPL policies and of SMT-LIB files enabling the automatic analysis of policies. The Java FACPL library provides the compile- and run-time support for validating and enforcing the generated Java policies in real systems. The use of the SMT-LIB code and of the Z3 constraint solver offers effective analysis means. Furthermore, the toolchain offers a (partial) interoperability with the XACML standard, commonly used to deploy real-world access control systems. See Section 9.1 of this FACPL paper for further details on XACML vs. FACPL interoperability.

FACPL Evaluation Process

Policies control system resources by means of a particular evaluation process, which relies on two main components: the Policy Decision Point (PDP) and the Policy Enforcement Point (PEP). The former calculates the authorization decision for an access request, and the latter enforces such decision in the system. Figure 2 shows the FACPL evaluation process.


Figure 2. FACPL Evaluation Process

Each controlled resource is paired with one or more FACPL policies, which define the access control rules expressing the credentials necessary to gain access to the resource. These policies are stored within the Policy Repository (PR) that makes them available to the PDP (step 1), which has the task of deciding whether to grant access to resources or not. The evaluation of a request is organized in the following steps.

Notably, obligations are additional actions connected to the access control system and might correspond to, e.g., updating a log file, sending a message, generating an event or executing an action.

Download and Installation

The FACPL language has the dedicated web site facpl.sourceforge.net that provides a full account of the language and its supporting tools. From the web site, it is also accessible the "Try FACPL in your Browser" web application, that allows newcomer users to experiment with FACPL without installing any software. A set of FACPL examples are available on the web application and for download, together with the corresponding Java-translated policies, in the code repository. The binaries and source code of the Java library and its unit tests can be downloaded from the repository as well.

The Eclipse plugin is provided by means of the Eclipse Update Site http://facpl.sourceforge.net/release/2.0.4/ (the current stable version is the 2.0.4). Thus, by using the well-known procedure "Install new software..." from the Eclipse's toolbar menu, the FACPL plugin can be easily installed. Note that it is required to accept the Eclipse Public License in order to complete the installation. The plugin installation requires:

If the Xtext plugins are missing, they will be automatically added through the standard Eclipse update site, e.g., the http://download.eclipse.org/releases/mars in case of Eclipse Mars. The plugin has been successfully tested by using the Eclipse DSL Release Mars 4.5.1.

Using the tool

When the installation of the plugin has completed, we can create a FACPL project to start coding, analysing and evaluating FACPL policies. Below, we briefly outline the creation of FACPL projects and files, introduce the syntax and semantics of FACPL, its analysis, and conclude by presenting commands and features of the plugin.

Setting Up a FACPL Project

A FACPL project can be created from the project menu "File -> New Project ...", where the customised wizard FACPL Development Project is available. After choosing a project name, the wizard creates a new Java Plugin-Development Project that contains all the required libraries for the coding and evaluation tasks; note that the project name cannot contain any blank space.


Figure 3. A FACPL Project

The generated FACPL project is like the one reported in Figure 3. FACPL files are generic text files having the ".fpl" extension and, for practical convenience, are placed in the src-facpl folder; a policy demo is added to the auto-generated project. The FACPL Java-translated policies and requests are automatically placed in the src folder. Instead, the src-xml folder contains the generated XML files and the src-smtlib folder contains the generated SMT-LIB files.

A new FACPL file can be created either as a new generic file with extension ".fpl" or by using the FACPL File wizard from the command File -> New... in the menu. The wizard permits specifying the container of the file (by selecting it from the projects available in the workspace), the name of the file, and some basic code examples to add to the new file.

Policy Specification

A FACPL file is composed of three different parts (for which the new file wizard provides basic templates):

An access control policy is hierarchically structured in terms of rules and policy sets, where a rule is a basic element for specifying access controls, while a policy set is a collection of other policies.

A rule specifies a name, the positive or negative decision of its successful evaluation (i.e., permit or deny), and a target expression for checking the applicability with respect to a request.

A target is a boolean expression defining the conditions deciding if the enclosed policy has to authorised an incoming request. The expressions are formed by basic relational and arithmetic operators. Such opertors define conditions on requests by means of attribute name. The available operators and some special attribute names (e.g. to get the current time) are provided by the auto-completion feature (e.g., for Mac/s users ⌘+Space) of the plugin. Attribute names are of the form Identifier/Identifier, where the first identifier stands for a category name and the second for an attribute name. For example, the name action/action-id represents the value of the attribute action-id within the category action. Notably, the plugin provides a type inference system checking that the expressions are correctly typed.

A policy set specifies a name, the combining algorithm to be used for combining the results of the contained policies, and a target expression for defining its applicability. The available combining algorithms are: permit-overrides, deny-overrides, permit-unless-deny, deny-unless-permit, first-applicable, only-one-applicable, weak-consensus and strong-consensus. The behaviour of each of them is presented in Policy Evaluation. Each algorithm is paired with a fulfilment strategy, i.e. all or greedy, leading its evaluation (see below). In addition, if different behaviours are requested, it is also possible to specialise the custom-algorithm. Furthermore, the command include permits to add, by means of name reference, a policy set to another one.

Each of the previous elements can also include a list of obligations. An obligation specifies an effect, i.e. permit or deny, for the applicability of the obligation, a type, i.e. M for Mandatory and O for Optional, and the identifier of an action with its argument. These arguments are generic expressions possibly containing attribute names, while the set of action identifiers understood by the PEP can be chosen, from time to time, according to the specific application.

The definition of the policy authorisation system (PAS), in addition to the access control policies defining the PDP, defines the top-level combining algorithm for the PDP (i.e., one among the algorithms already mentioned) and the enforcement algorithm for the PEP (i.e., one among base, permit-biased and deny-biased).

The following figure reports an example of policy declaration from an e-Health case study.


Figure 4. Example of FACPL Policy

The policy manages all the requests for the management of the e-Prescription service of the patient named 'Alice'. The rules checks the credentials exposed by the requester (i.e., the permission) and the requested actions.

We briefly comment part of the reported policy. The policy named "ePre" checks, by means of its target, if the requested service is "e-Prescription", then the internal rules check the exposed credentials according to the requested actions. By way of example, the rule named "writeDoc" authorises with permit (i.e., a positive authorisation) a subject whose role is doctor (i.e., by using attribute subject/role) and whose permissions contain both the permissions "e-Pre-Read" and "e-Pre-Write". Notably, the rules are evaluated in the same order as they appear within the policy. Thus, since the chosen combining algorithm is permit-overrides (see below), if the first rule evaluates correctly (i.e. it returns permit) then the second rule is not evaluated. Finally, the obligation log is used to record in the system the authorised access. The other rules are similarly defined, as well as the obligation mailTo.


Figure 5. Example of FACPL Request

Figure 5 reports an example of FACPL request. Specifically, it represents the "doctor" with id "Dr. House" and credentials "e-Pre-Read" and "e-Pre-Write", willing to "write" an "e-Prescription" for the patient with id "Alice". This request is authorised to permit by the previous policy.

Policy Evaluation

The evaluation of a request with respect to a policy generates one among the following authorization decisions:

When the resulting authorisation decision is permit or deny some obligations can possibly be present.

The evaluation of a policy with respect to a request starts by checking its applicability to the request, which is done by evaluating the expression defining its target. Evaluating expressions amounts to apply operators and to resolve the attribute names occurring within, that is to determine the value corresponding to each such name. If this is not possible, i.e. an attribute with that name is missing in the request and cannot be retrieved through the context handler, the special value ⊥ is returned. This value can be explicitly managed by the various operators. The evaluation of a policy has indeed the following cases: Clearly, a policy with target expression true (resp., false) applies to all (resp., no) requests. The evaluation process of rules and policy sets is summarised, respectively, in Tables 1 and 2.

TargetObligationRule Result
truefulfilledrule effect + FO
truefulfilment errorindeterminate
false or ⊥ - not-applicable
error or non-boolean value -indeterminate
Table 1. Rule evaluation (where FO stands for 'fulfilled obligations')

TargetCombining AlgorithmObligationPolicy Set Result
truepermit (resp., deny)fulfilledpermit (resp., deny) + FO
truenot-applicable-not-applicable
trueindeterminate-indeterminate
truepermit (resp., deny)fulfilment errorindeterminate
false or ⊥ - - not-applicable
error or non-boolean value - - indeterminate
Table 2. Policy set evaluation (where FO stands for 'fulfilled obligations')

Concerning the evaluation of expressions, it takes into account the types of the operators arguments, and possibly returns the special value ⊥ and error. In details, if the arguments are of the expected type, the operator is applied, else, i.e. at least one argument is error, error is returned; otherwise, i.e. at least one argument is ⊥ and none is error, ⊥ is returned. The expression operators and and or enforce a different treatment of these special values. Specifically, and returns true if both operands are true, false if at least one operand is false, ⊥ if at least one operand is ⊥ and none is false or error, and error otherwise (e.g. when an operand is not a boolean value). The operator or is the dual of and. Hence, and and or may mask ⊥ and error. Instead, the unary operator not only swaps values true and false and leaves ⊥ and error unchanged. The other expression operators have the expected semantics (e.g., operator equal checks if the arguments are equal) and enforce the management strategy for the special values ⊥ and error possibly resulting from the evaluation of their arguments. Indeed, they establish that error takes precedence over ⊥ and is returned every time the operator arguments have unexpected types; whereas ⊥ is returned when at least an argument is ⊥ and there is no error.

The evaluation of a policy includes the fulfilment of the enclosed obligations whose applicability effect coincides with the decision calculated for the policy. The fulfilment of an obligation consists in evaluating all the expression arguments of the enclosed action. If an error occurs, the policy decision is changed to indet. Otherwise, the fulfilled obligations are paired with the policy decision to form the PDP response.

The behaviour of the combining algorithms available in the plugin is as follows:

Each algorithm is paired with a fulfilment strategy, i.e. one between all and greedy. The greedy strategy may significantly improve the evaluation performance of a sequence of several policies.

Finally, the custom-algorithm doesn't implement any behaviour; when the Java code is generated, it only returns a "template" for implementing a customised combining algorithm.

The authorisation decision resulting from the PDP evaluation is then enforced by means of the chosen enforcement algorithm according to the results of the execution of obligations. The behaviour of each enforcement algorithm is as follows:

Notably, errors possibly occurring while discharging optional obligations are ignored, so that they do not affect the enforcement process.

Policy Analysis

To analyse FACPL policies, it is used an approach based on constraints. The automatic verification of such constraints is obtained through an SMT solver, like, e.g., Z3. For additional details on how such constraints are generated see this FACPL paper The type of properties we can check on policies by means of such constraints are:

Plugin Commands and Facets

The FACPL plugin offers many facets to support policy development, from the organisation of code to commands for generating Java and XML code.

Navigation and formatting. The multi-page editor highlights FACPL keywords and policies' structure defining various formatting layouts for policy elements (i.e., combining algorithms, keywords, effects, and literals), and an auto-indentation command for FACPL code. The latter command can be invoked by using the classical Eclipse shortcut ⌘+Shift+F (or Ctrl+Shift+F for Window's users). Furthermore, the structure of policies can be also navigated by means of the Outline View specifically designed for FACPL specifications.

Scope and Import. The scope of a file is the set of requests and policies defined inside the file. The scope is used to check the references of requests and policies in the Eval Request option and in the include command, respectively.

The plugin allows the developers to split the code in different modules and, by using import commands, to create cross-file scope for policies and requests. The import is defined as the command import 'name_file.fpl' and can access all the FACPL files in the current folder. Therefore, the scope of the file where the import is defined is extended with the scope of the imported files. Specifically, all requests and policies defined in the imported file are also visible in the current file.

Name checks. For policies and policy sets it is ensured the uniqueness of names. This check is performed among policy items together with policy set ones, because both of them can be used in an include command. Moreover, when an import command is present, the name check verifies uniqueness of local items with respect to the imported ones.

Generation parameters. The meaning of the attributes defined in the Main Attributes section of the FACPL code is as follows:

When these options are properly selected, the generation of Java code defines, in the PEP Java class, the main method for running requests' evaluation.

Generation of Java Code. To generate the corresponding Java code of a FACPL specification, the IDE provides the command Generate Java Code from FACPL in the pop-up menu (right click in the editor or on the specific file in the package explorer view) and in the FACPL toolbar menu. The resulting Java classes will be included in the package defined in the main attributes. If there are one or more imported files, the generation command is recursively executed on those FACPL files.

Generation of XACML (XML) policies. From the FACPL code it is also possible to generate the corresponding XACML files written as XML code. The command Generate XACML Code from FACPL in the pop-up menu or in the FACPL toolbar menu generates the corresponding XML files into the src-xml folder.

Generation of SMT-LIB. From the FACPL code it is also possible to generate the corresponding SMT-LIB code. The command Generate SMT-LIB Code from FACPL in the pop-up menu or in the FACPL toolbar menu generates the corresponding SMT-LIB file into the src-smtlib folder. This file can then pass as input to an SMT solver like, e.g., Z3.

Policy Analysis. The menu commands Create Authorisation Property... and Create Structural Property... provide a guided interface to create the SMT-LIB file needed to check the satisfiability of the chosen authorisation and structural property, respectively.

FAQ

Contacts

For any problem or questions, add an issue to the GitHub repository or mail to andrea.margheri@unifi.it.

References