Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Verification of Robust Properties for Access Control Policies

Alexander V. Gheorghiu

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}φ$ stating that policy $P$ has robust property $φ$, 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.

Verification of Robust Properties for Access Control Policies

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 stating that policy has robust property , 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.
Paper Structure (25 sections, 4 theorems, 21 equations, 1 figure)

This paper contains 25 sections, 4 theorems, 21 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Background
  3. Logic and Access Control Policies
  4. Verification of Access Control Policies
  5. Running Example: Conference Management
  6. Specification of Robust Properties
  7. Support, Derivability, and Policy Extension
  8. Policy extension.
  9. Implication.
  10. Disjunction: Reasoning Under Pending Alternatives
  11. Conjunction: Compound Security Requirements
  12. Negation: Policy Corruption
  13. Summary: The Support Judgment
  14. Inferentiality.
  15. Modal character.
  16. ...and 10 more sections

Key Result

Proposition 6

If $\Vdash_\mathcal{P} \phi$ and $\mathcal{P} \supseteq \mathcal{Q}$, then $\Vdash_\mathcal{Q} \phi$.

Figures (1)

  • Figure 1: Support judgment clauses for robust properties.

Theorems & Definitions (15)

  • Example 1: Conference Management System
  • Example 2: Delegation implies authority check
  • Example 3: Separation of duty under pending appointment
  • Example 4: Compound delegation constraint
  • Example 5: Conflict of interest as incompatibility
  • Proposition 6: Monotonicity
  • proof
  • Lemma 7: Cut
  • Lemma 8: Monotonicity
  • Example 9: Conference Policy as a Logic Program
  • ...and 5 more