Verification of Robust Properties for Access Control Policies

TL;DR

This paper introduces a new method for verifying access control policies that ensures properties hold regardless of how policies are extended or decisions are made, enabling more flexible and reliable security policy verification.

Contribution

It defines a robust property verification framework for access control policies, proving its compositionality and providing a sound, complete, and executable verification procedure.

Findings

Verification reduces to second-order logic programming.

Properties are preserved under policy extension.

The method is both sound and complete.

Abstract

Existing methods for verifying access control policies require the policy to be complete and fully determined before verification can proceed, but in practice policies are developed iteratively, composed from independently maintained components, and extended as organisational structures evolve. We introduce robust property verification: the problem of determining what a policy's structure commits it to regardless of how pending decisions are resolved and regardless of subsequent extension. We define a support judgment $\Vdash_{P}\phi$ stating that policy $P$ has robust property $\phi$, with connectives for implication, conjunction, disjunction, and negation, prove that it is compositional (verified properties persist under policy extension by a monotonicity theorem), and show that despite quantifying universally over all possible policy extensions the judgment reduces to proof search in a second-order logic programming language. Soundness and completeness of this reduction are established, yielding a finitary and executable verification procedure for robust security properties.