The Formal Access Control Policy Language (FAPCL) is a formally-defined language for the specification, analysis and enforcement of attribute-based access control policies. FACPL has a compact and intuitive syntax and is equipped with Java-based tools, comprising a dedicated Eclipse plugin and a ready-to-use web application.
The language has been designed within the EU project ASCENS with the aim of regulating the authorisation of the interactions of autonomic components.
Why a formal language?
The language is equipped with a formal denotational semantics that has permitted us to precisely define intricate aspects of attribute-based access control (e.g., missing attributes, combining algorithms, obligations) and to prove the correctness of the devised analysis approaches.
The formal semantics has also been used to lead the development of the Java-based tools by means of test-driven modelling approach.
How use FACPL?
FACPL is supported by a Java-based toolchain. All the functionalities are brought together through an Eclipse-based Integrated Development Environment (IDE). Indeed, the IDE facilitates developers via graphical supporting features, e.g., auto-completion and auto-generation of runnable Java code. Moreover, the IDE offers effective analysis services via the Z3 constraint solver and (partial) interoperability with XACML.
The FACPL toolchain is represented in the following figure.
FACPL can be experimented directly in the browser via a web application