Verification of Robust Properties for Access Control Policies

• URL: http://arxiv.org/abs/2603.13181v1
• Date: Fri, 13 Mar 2026 17:14:38 GMT
• Title: Verification of Robust Properties for Access Control Policies
• Abstract summary: Existing methods for verifying access control policies require the policy to be complete and fully determined before verification can proceed.<n>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.<n>We show that despite quantifying universally over all possible policy extensions the judgment reduces to proof search in a second-order logic programming language.
• Score: 51.736723807086385
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Policy Loopholes in Agent Evaluation: When Policy Ambiguity Masquerades as Agent Error [2.0305676256390934]
  Benchmark developers should audit policies before collecting gold annotations.<n>A cross-domain comparison reveals that exploitability requires both policy ambiguity and tool permissiveness.
  arXiv  Detail & Related papers  (2026-09-13T10:00:13Z)
• From Intent to Execution Grant: An Execution-Boundary Conformance Profile for High-Risk AI Actions [9.27474112226667]
  EBL-Core decides whether one canonical, fully materialized AI-generated candidate may receive action-scoped execution authority under explicit conditions.<n>It binds, policy non-weakening, evidence handling, deterministic adjudication, verification, and grant lifecycle behavior.<n>Across 100 trials, 32 concurrent Redemption attempts yielded exactly one successful Redemption and protected test effect per trial.
  arXiv  Detail & Related papers  (2026-09-10T14:21:45Z)
• Interpretable reinforcement learning with decision-tree pruning [0.0]
  Reinforcement learning policies are difficult to inspect, but interpreting them is a prerequisite for trustworthiness.<n>We present a pruning process that simplifies such rule-based policies while preserving task performance.<n>We investigate this approach on classic control and MuJoCo benchmarks, where pruning traces reveal consistent interpretability improvements.
  arXiv  Detail & Related papers  (2026-08-07T12:14:33Z)
• PolicyBank: Evolving Policy Understanding for LLM Agents [51.86716874651299]
  PolicyBank maintains structured, tool-level policy insights and iteratively refines them.<n>PolicyBank closes up to 82% of the gap toward a human oracle.
  arXiv  Detail & Related papers  (2026-04-16T20:29:30Z)
• Runtime Governance for AI Agents: Policies on Paths [4.111929395230638]
  We argue that the execution path is the central object for effective runtime governance.<n>In our view, runtime evaluation is the general case, and it is necessary for any path-dependent policy.
  arXiv  Detail & Related papers  (2026-03-17T14:35:52Z)
• An Extended Consent-Based Access Control Framework: Pre-Commit Validation and Emergency Access [0.0]
  Consent-Based Access Control (CBAC) is a foundational mechanism for enforcing patient autonomy in modern healthcare information systems.<n>This paper presents an extended CBAC framework that enforces semantic correctness at consent creation time rather than during access evaluation.
  arXiv  Detail & Related papers  (2026-03-07T02:55:00Z)
• Convergence and Sample Complexity of First-Order Methods for Agnostic Reinforcement Learning [66.4260157478436]
  We study reinforcement learning in the policy learning setting.<n>The goal is to find a policy whose performance is competitive with the best policy in a given class of interest.
  arXiv  Detail & Related papers  (2025-07-06T14:40:05Z)
• Learning Deterministic Policies with Policy Gradients in Constrained Markov Decision Processes [59.27926064817273]
  We introduce an exploration-agnostic algorithm, called C-PG, which enjoys global last-iterate convergence guarantees under domination assumptions.<n>We empirically validate both the action-based (C-PGAE) and parameter-based (C-PGPE) variants of C-PG on constrained control tasks.
  arXiv  Detail & Related papers  (2025-06-06T10:29:05Z)
• Few-shot Policy (de)composition in Conversational Question Answering [54.259440408606515]
  We propose a neuro-symbolic framework to detect policy compliance using large language models (LLMs) in a few-shot setting.<n>We show that our approach soundly reasons about policy compliance conversations by extracting sub-questions to be answered, assigning truth values from contextual information, and explicitly producing a set of logic statements from the given policies.<n>We apply this approach to the popular PCD and conversational machine reading benchmark, ShARC, and show competitive performance with no task-specific finetuning.
  arXiv  Detail & Related papers  (2025-01-20T08:40:15Z)
• Bounded Robustness in Reinforcement Learning via Lexicographic Objectives [54.00072722686121]
  Policy robustness in Reinforcement Learning may not be desirable at any cost. We study how policies can be maximally robust to arbitrary observational noise. We propose a robustness-inducing scheme, applicable to any policy algorithm, that trades off expected policy utility for robustness.
  arXiv  Detail & Related papers  (2022-09-30T08:53:18Z)
• Cross-Policy Compliance Detection via Question Answering [13.373804837863155]
  We propose to address policy compliance detection via decomposing it into question answering. We demonstrate that this approach results in better accuracy, especially in the cross-policy setup. It explicitly identifies the information missing from a scenario in case policy compliance cannot be determined.
  arXiv  Detail & Related papers  (2021-09-08T15:47:41Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.