On Properties of Policy-Based Specifications

TL;DR

This paper investigates the effectiveness of policy-based specifications in enforcing security properties in complex systems, formalizes relevant structural properties, and demonstrates automated verification through a banking case study.

Contribution

It advances understanding of policy-based security specifications by formalizing structural properties and proposing automated verification methods with practical case studies.

Findings

Policy-based specifications can effectively enforce security properties.

Formalization of structural properties aids in policy analysis.

Automated verification approach is feasible in real-world scenarios.

Abstract

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.