Access Control as Verified Parse Constraints

• URL: http://arxiv.org/abs/2609.12488v1
• Date: Fri, 11 Sep 2026 06:33:41 GMT
• Title: Access Control as Verified Parse Constraints
• Abstract summary: Security gateways repeatedly ship implementation bugs in the code path between the network and the policy decision.<n>Existing approaches either leave the enforcement unverified or connect a formal model to a hand-written engine only by differential testing.<n>Our contribution is a class result: a forward-only, backtrack-free EverParse validator.
• Score: 2.230473633870735
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Commercial security gateways repeatedly ship implementation bugs in the code path between the network and the policy decision: hand-written enforcement logic that diverges from the policy author's intent, and ad-hoc request parsers at the network boundary that introduce memory-safety flaws of their own. In both cases the bug is in the deployed enforcement code, not in the policy. Existing approaches either leave the enforcement runtime unverified or connect a formal model to a hand-written engine only by differential testing. Our contribution is a class result: a forward-only, backtrack-free EverParse validator is a verified recognizer for a bounded, finite-state class, and access-control decision functions with fixed-offset fields and bounded disjunction belong to it, so one machine-checked proof transfers to every policy in the class rather than being re-established per policy. Concretely, we encode a bounded policy language's decision function into a fixed-size byte buffer and verify the enforcement code once---covering all byte values---with an SMT solver, proving the validator accepts if and only if the decision function accepts, for every policy, request, and session. Editing rule content over a fixed endpoint set then needs no new proof; adding endpoints reruns the toolchain; extending the language needs new proofs. We establish faithful enforcement of a policy, not that a policy is itself secure. The verified gate is platform-independent, requiring only EverParse/Z3 and a C compiler, whose correctness we assume. We demonstrate a deployment on the seL4 microkernel, which ensures every request passes through the gate and that unverified components cannot corrupt the verified enforcement chain.

Related papers

• PolicyMem: Geometric Policy Memory for LLM Governance [72.04962480384322]
  We introduce PolicyMem, a geometric policy memory that externalizes natural-language policies as reusable geometric memory objects.<n>A memory writer compiles natural-language policies into policy memory slots, and query-response pairs read the policy memory through projection energy.<n>The resulting policy-evidence profile directly mediates the safety verdict and is reused for policy attribution and post-intervention verification.
  arXiv  Detail & Related papers  (2026-09-12T06:07:43Z)
• LMSM: LLM Security Framework Inspired by Linux Security Modules [56.93644694627783]
  Large language models (LLMs) are increasingly deployed with layered defenses, yet malicious prompts can still bypass them.<n>We present Language Model Security Modules (LMSM), a security framework that adapts the separation behind Linux Security Modules (LSM) to LLM serving.
  arXiv  Detail & Related papers  (2026-08-26T12:13:05Z)
• Falsifiable Release Gates for Self-Improving Systems [0.0]
  We describe falsifiable release gates, and a methodology to build and validate such systems.<n>Every new capability must pass a pre-specified, machine-verifiable acceptance suite before it ships.<n>No action goes to an effector without a safety-critical property capability token minted by a control ring.
  arXiv  Detail & Related papers  (2026-07-11T06:06:34Z)
• AutoCedar: An Agentic Framework for Verifier-Guided Access Control Policy Synthesis [0.2449909275410288]
  AutoCedar is a verifier-guided system that turns natural-language access-control requirements into a reviewed, checkable target.<n>It then synthesizes Cedar policies against that target.
  arXiv  Detail & Related papers  (2026-07-04T01:13:32Z)
• VIGIL: Runtime Enforcement of Behavioral Specifications in AI Agent Skills [13.980239249972819]
  VIGIL is an end-to-end runtime enforcement framework for agentic systems.<n>It checks an agent's actual execution trace against behavioral policies from skill specifications, operator-defined constraints, and global rules spanning multiple skills.<n>It detects policy violations with over 95% recall and a false-positive rate below 10%.
  arXiv  Detail & Related papers  (2026-06-25T01:58:44Z)
• LiSA: Lifelong Safety Adaptation via Conservative Policy Induction [45.88278850743155]
  guardrails are no longer merely answer-quality: they can leak secrets, authorize unsafe actions, or block legitimate work.<n>LiSA is a conservative policy induction framework that improves a fixed base guardrail through structured memory.<n>Ultimately, LiSA offers a practical path to secure AI agents against the unpredictable long tail of real-world edge risks.
  arXiv  Detail & Related papers  (2026-05-14T06:47:35Z)
• Skills as Verifiable Artifacts: A Trust Schema and a Biconditional Correctness Criterion for Human-in-the-Loop Agent Runtimes [0.0]
  We argue that a skill is emphuntrusted code until it is verified.<n>Without skill verification, a human-in-the-loop gate must fire on every irreversible call.<n>We give a trust schema that includes an explicit verification level on every skill manifest.
  arXiv  Detail & Related papers  (2026-05-01T05:53:05Z)
• 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)
• Compiling Activation Steering into Weights via Null-Space Constraints for Stealthy Backdoors [48.881343993730844]
  Safety-aligned large language models (LLMs) are increasingly deployed in real-world pipelines.<n> adversaries can distribute backdoored checkpoints that behave normally under standard evaluation but jailbreak when a hidden trigger is present.<n>Recent post-hoc weight-editing methods offer an efficient approach to injecting such backdoors.
  arXiv  Detail & Related papers  (2026-04-14T06:48:33Z)
• Verification of Robust Properties for Access Control Policies [51.736723807086385]
  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.
  arXiv  Detail & Related papers  (2026-03-13T17:14:38Z)
• Conformal Policy Control [50.46542384484142]
  We show how to use any safe reference policy as a probabilistic regulator for any optimized but untested policy.<n>Unlike conservative optimization methods, we do not assume the user has identified the correct model class.<n>Our experiments on applications ranging from natural language question answering to biomolecular engineering show that safe exploration is possible from the first moment of deployment.
  arXiv  Detail & Related papers  (2026-03-02T18:54:36Z)
• QuadSentinel: Sequent Safety for Machine-Checkable Control in Multi-agent Systems [22.833567409552074]
  textscQuadSentinel is a four-agent guard that compiles safety policies into machine-checkable rules.<n>textscQuadSentinel improves guardrail accuracy and rule recall while reducing false positives.
  arXiv  Detail & Related papers  (2025-12-18T07:58:40Z)

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.