On Properties of Policy-Based Specifications
This work addresses the problem of improving security and maintainability in access control systems for system designers, but it is incremental as it builds on existing policy-based approaches.
The paper tackles the challenge of securing access in complex computing systems by studying how policy-based specifications enforce traditional security properties, and formalizes structural properties of policies to aid system designers, with a case study from banking demonstrating real instances and an approach for automated verification.
The advent of large-scale, complex computing systems has dramatically increased the difficulties of securing accesses to systems' resources. To ensure confidentiality and integrity, the exploitation of access control mechanisms has thus become a crucial issue in the design of modern computing systems. Among the different access control approaches proposed in the last decades, the policy-based one permits to capture, by resorting to the concept of attribute, all systems' security-relevant information and to be, at the same time, sufficiently flexible and expressive to represent the other approaches. In this paper, we move a step further to understand the effectiveness of policy-based specifications by studying how they permit to enforce traditional security properties. To support system designers in developing and maintaining policy-based specifications, we formalise also some relevant properties regarding the structure of policies. By means of a case study from the banking domain, we present real instances of such properties and outline an approach towards their automatised verification.