PaperlayerView exact revision on arXiv

Source-linked AI summary

Formal Policy Enforcement for Real-World Agentic Systems

Nils Palumbo, Sarthak Choudhary, Jihye Choi, Guy Amir, Prasad Chalasani, Somesh Jha

arXiv:2602.16708v3cs.CRcs.AIcs.MA

TL;DR

Agentic systems commonly rely on prompt-embedded policies and agent reasoning, leaving enforcement without formal guarantees for cross-agent, history-dependent decisions. The paper introduces FORGE, an aspect-oriented runtime framework using Datalog policies, contracted observability, and a reference monitor. Across three case studies, FORGE eliminates policy violations while preserving task success, with modest overhead, subject to its stated instrumentation and translation limitations.

  • Problem

    Prompt-embedded policies provide no formal enforcement guarantee and do not adequately express policies dependent on causal history across multiple agents.

  • Method

    FORGE weaves Datalog policies into agentic systems, using an assume/guarantee observability contract and a reference monitor to enforce decisions without modifying agents.

  • Results

    FORGE eliminates policy violations while preserving task success across three quantitative case studies, including attack success falling from 100% to 0% and compliance rising from 58% to 98%.

  • Takeaways & Limitations

    Formal runtime enforcement can provide policy guarantees for multi-agent deployments while retaining task success at modest runtime overhead.

  • Takeaways & Limitations

    The framework’s guarantees depend on instrumented channels, an uncompromised trusted base, and faithful policy translation; improving translation remains future work.

Abstract

from arXiv · show

Security policy enforcement in contemporary agentic systems predominantly consists of embedding natural-language policies within an agent's system prompt and delegating compliance to the agent's reasoning. This approach admits no formal enforcement guarantee and cannot express policies whose satisfaction depends on the causal history of an execution, a gap that becomes acute in multi-agent systems, where enforcement must reason across agents. We argue that policy enforcement in agentic systems is most naturally understood as a cross-cutting concern, and propose a framework grounded in aspect-oriented programming that specifies policies independent of the agent's reasoning and enforces them at every policy-relevant decision. Policies are written in Datalog over a set of abstract predicates describing the execution context, an observability service governed by a formal assume/guarantee contract maintains these predicates, and a reference monitor consults the policy at each action to produce an enforcement decision. When the environment contract holds, enforcement decisions coincide with the policy's intended semantics. We adopt Datalog as the policy language, a natural fit because it supports declarative rule specification, admits recursion for policies over transitive relationships, and yields deterministic enforcement. Datalog further admits tractable static analyses for contradiction, redundancy, subsumption, and conditional reachability, enabling authors to verify policy intent and surface ambiguities inherent in natural-language specifications. We realize the framework in FORGE, which enforces policies over agentic deployments without modification to the underlying agents. We evaluate FORGE on three case studies: information flow policies for prompt injection defense, approval workflows in a multi-agent pharmacovigilance system, and organizational policies for customer service.

1 Introduction

Agentic systems need policy enforcement that operates across agents and execution history rather than relying on natural-language instructions and agent compliance. The paper proposes FORGE, an aspect-oriented framework using Datalog, contracted observability, and runtime reference monitoring, and evaluates it across three case studies.

  • Motivation: Prompt-based policies provide no formal enforcement guarantees and are poorly suited to multi-agent, partially ordered executions.Existing approaches typically rely on agents to follow natural-language instructions and enforce policies over linear traces.
  • Framework: Policy-relevant events span agents, models, services, and tools, making enforcement a cross-cutting concern.The framework therefore applies Aspect-Oriented Programming to separate policy enforcement from agent logic.
  • Policy Language: Datalog provides declarative, recursive, deterministic policy evaluation and separates formal rules from natural-language policy sources.A separate translation stage produces Datalog rules grounded in the deployment substrate and attaches clause-level source annotations for validation.
  • Framework: FORGE represents execution context with abstract predicates maintained by an observability service and evaluates policies at each candidate action through a reference monitor.The monitor’s correctness depends on an explicit environment contract that exposes relevant events, dependencies, identities, and external state.
  • Evaluation: Prompt-injection attack success drops from 100% to 0%, τ2-bench compliance rises from 58% to 98%, and unauthorized FDA accesses fall from 40 to 0.Across three quantitative case studies, FORGE eliminates policy violations while preserving task success; end-to-end latency rises by 19–38% and per-trial cost increases remain below $0.05.

2 Setup and Threat Model

The paper models agentic systems as entities producing messages, tool invocations, and tool results through state transitions. FORGE treats agents and external content as untrusted, while its guarantees depend on trusted enforcement components and exclude uninstrumented channels and compromised infrastructure.

  • Agentic System: An agentic system consists of entities whose operations generate traces containing messages, tool invocations, and tool results.The model makes no assumptions about entity internals and defines these event kinds as the observable behavior.
  • Execution Model: Executions proceed through state transitions in which each event extends the current state with its causal dependencies.Events become available as inputs to later steps, and the final state records the execution history.
  • Authorization: Only externally side-effecting or security-sensitive events in A require authorization; other events update state without invoking a decision.Tool invocations are typical actions, but messages and tool results may also qualify when they trigger external effects.
  • Threat Model: The threat model treats agents, tool outputs, and external content as untrusted, while FORGE components and correctly executing policies form the trusted computing base.Untrusted entities may behave arbitrarily, including manipulating prompts, tool outputs, or external inputs.
  • Scope: FORGE does not cover attacks that compromise trusted components, bypass the instrumented event surface, or target the underlying infrastructure.Such defenses belong to adjacent layers including sandboxing, network isolation, and hardened runtimes.

3 Policy Enforcement as Aspect Weaving

FORGE casts authorization as aspect weaving: policies select candidate actions through substrate predicates, and a reference monitor allows or denies each matched action. Under the environment contract, runtime verdicts coincide with intended policy semantics and denied actions do not execute.

  • Aspect-Oriented Formulation: Authorization is cross-cutting because every candidate action must be checked against context accumulated across the execution.The aspect-oriented formulation separates enforcement from individual entity logic.
  • Aspect-Oriented Formulation: In FORGE, candidate actions are join points, policy conditions are pointcuts, and reference-monitor computations are advice producing Allow or Deny verdicts.The weaver inserts this advice without modifying entity internals.
  • Enforcement Discipline: The weaver suspends each authorized action until the reference monitor evaluates the policy, allowing it to proceed only on Allow.Denied actions do not execute, and optional feedback is returned to the calling entity.
  • Policy Substrate: The policy substrate supplies typed predicates for roles, causal provenance, and deployment-specific concepts, populated by the environment.These externally supplied predicates form policy inputs, while derived predicates are defined within the policy.
  • Policies: Datalog policies combine positive and negated literals, joins, recursion, authorization rules, and reusable auxiliary predicates.Evaluation closes the substrate state under the policy with the candidate action bound to the action variable.
  • Correctness: Under the environment contract, FORGE’s runtime decisions coincide with intended policy semantics, so actions with intended verdict Deny never execute.The theorem localizes trust in the environment contract; once discharged, the remaining enforcement machinery is correct by construction.

4 Policy Specification in Datalog

Section 4 selects Datalog as a formal policy language because it combines expressive authorization rules, efficient deterministic evaluation, and policy analysis. It also describes translation from natural-language policies and the checks used to validate the resulting formal rules.

  • Language choice: Datalog is chosen to support expressive authorization conditions, efficient action-time decisions, and analyzable policy artifacts.The design requirements distinguish enforcement necessities—expressivity and decidability/efficiency—from analyzability, which makes policies reviewable.
  • Language choice: Recursive predicates express unbounded supervisory relationships that fixed-depth conjunctive rules cannot finitely encode.The recursive Supervises rules define the transitive closure of Manages, allowing approval conditions over arbitrary reporting-chain depth.
  • Policy analysis: Static analyses detect contradictions, redundancies, and related policy defects through query-containment or reachability checks without executing the system.These analyses operate on a non-recursive fragment because containment over fully recursive Datalog is undecidable in general.
  • Running example: The running policy allows FDA submissions only when the requester has the required role, the action has approval, and the approver supervises the requester.Its rule combines action structure, identity, approval provenance, and the recursively derived Supervises predicate.
  • Translation: Natural-language policies are translated into substrate-grounded Datalog programs with clause-level annotations supporting coverage and entailment checks.The translator itself has no formal correctness guarantee, so the validation pipeline identifies omitted, fabricated, or distorted rules and supports revision.
  • Translation: The translation pipeline is intended to establish source fidelity, while strengthening the translator and validation pipeline remains future work.The paper distinguishes fidelity validation from runtime correctness of the deployed formal policy.

5 FORGE

FORGE implements the framework as an aspect weaver, observability service, and reference monitor that mediate tool invocations without changing agent reasoning. It records causal dependencies, evaluates policies over the resulting substrate, and releases actions only after an allow verdict.

  • Architecture: FORGE combines a reference monitor, observability service, and aspect weaver to enforce Datalog policies during agent execution.The reference monitor evaluates candidate actions, the observability service supplies trace-derived predicates, and the weaver inserts mediation at tool-invocation boundaries.
  • Aspect weaving: The weaver intercepts tool calls between the agent loop and tool implementation while leaving agent reasoning, planning, memory, and permitted tool effects unmodified.Integration targets the tool-dispatch boundary rather than individual agents.
  • Observability service: The observability service builds a dependency graph by recording consumed messages, produced messages, event identifiers, and causal edges at message-producing join points.The same pattern applies to LLM calls and other message-producing methods, while action provenance is propagated to the action site.
  • Correctness conditions: FORGE’s observability guarantees cover instrumented join points, while behaviors such as raw sockets and stdio remain out of scope.The environment contract is discharged only over the instrumented surface.
  • Reference monitor: At each action join point, FORGE constructs an action descriptor, attaches an authentication witness, queries the policy engine, and dispatches only on Allow.Deny verdicts return structured feedback derived from policy-rule annotations.
  • Correctness conditions: Sound authorization requires each query to use the action’s complete backward slice, preventing stale provenance values under inter-agent or inter-task concurrency.FORGE synchronizes observability and policy evaluation to provide this substrate state.

6 Case Studies

FORGE is evaluated across prompt-injection defense, customer-service workflows, and multi-agent pharmacovigilance, comparing prompt-only policies with runtime enforcement. Runtime enforcement eliminates policy violations while preserving task success, with modest overhead and reasoning-dependent recovery.

  • Evaluation design: FORGE eliminates policy violations by construction while evaluating compliance, task success, and overhead across three quantitative case studies.The comparison uses non-instrumented agents given natural-language policies and instrumented agents enforced by a runtime reference monitor.
  • Scope of guarantee: FORGE guarantees policy compliance but does not improve agent reasoning, so incorrect recovery, planning, or interpretation can still cause task failure.When an action is blocked, the agent must interpret structured feedback and select a compliant alternative.
  • Information-flow policies: 100% attack success falls to 0% for prompt-injection trials, while benign task utility remains 5/5 under instrumentation.The study tests Bell-LaPadula MLS and toxic-flow policies over five trials each.
  • Customer-service policies: τ2-bench compliance improves from 58% to 98%, while the two failures across 90 instrumented trials are reasoning errors rather than policy violations.Instrumented agents maintain task success despite blocked actions, with recurring policy violations prevented by FORGE.
  • Pharmacovigilance approvals: All 40 unauthorized FDA accesses are eliminated, while instrumented MALADE trials achieve 15/15 correct predictions, matching the non-instrumented baseline.The 66 total blocks reflect fresh approval requirements for each DrugAgent–FDAHandler delegation session.

7 Related Work

FORGE combines reference monitoring, logic-based authorization, aspect-oriented programming, and provenance tracking into a unified framework for policy enforcement in multi-agent runtimes. Its stated contribution is an end-to-end correctness guarantee realized through the FORGE construction.

  • Reference monitoring: FORGE mediates agent tool invocations at runtime, extending reference-monitor and inline-monitoring strategies from operating-system or process boundaries to agentic systems.The monitored boundary is the agent’s tool-invocation interface.
  • Aspect-oriented enforcement: FORGE generalizes aspect-oriented policy weaving from individual programs to multi-agent runtimes spanning LLMs, agent loops, and inter-agent communication.The paper claims a correctness theorem at this level of generality that prior AOP-security work does not formalize.
  • Policy language: FORGE adopts Datalog with stratified negation, retaining decidable evaluation while adding a foreign-function discipline for content-level policy reasoning.This places the policy language within established logic-based authorization work while adapting it to agentic settings.
  • State and provenance: Unlike systems targeting stateless or weakly stateful resources, FORGE addresses authorization decisions that depend on causal execution history and multi-agent message flows.Its dependency graph represents events and causal edges consumed by the Datalog policy engine.
  • Synthesis: FORGE integrates established components into one framework whose end-to-end correctness is established by a theorem and realized by the implementation.The integrated components include reference monitors, logic-based authorization, Datalog, AOP, and provenance.

8 Discussion and Limitations

The discussion limits FORGE’s guarantees to instrumented execution surfaces and supported framework integrations. Extending coverage requires additional instrumentation, while policy translation remains partly dependent on manual verification and future tooling.

  • Mediation scope: FORGE makes no claims about behaviors that bypass instrumented tool dispatch and HTTP libraries, such as raw socket writes or stdio I/O.Additional channels require instrumentation of their issuance methods.
  • Framework extensibility: The current implementation targets specific agent frameworks, and adapting it to a new framework requires manually identifying dispatch and message-producing join points.The aspect templates are framework-agnostic, but enumerating the join-point set remains a manual step.
  • Policy authoring and translation: Case-study Datalog policies are generated by an LLM-based translator and then verified through manual review plus coverage and entailment checks.Improving translation robustness and automated policy authoring for non-experts remains future work.

9 Conclusion

FORGE combines aspect weaving, Datalog policies, observability, and reference-monitor enforcement to provide runtime policy enforcement for agentic systems. Its deployment mediates framework and direct external actions, while case-study rules enforce semantic and structural constraints.

  • Framework: FORGE combines aspect weaving, Datalog policies, an environment contract, observability, and a reference monitor for runtime enforcement.The framework maintains causal state and evaluates authorization at instrumented action points.
  • Implementation: The weaver supports framework-mediated tool calls and direct HTTP interactions without modifying agents’ core loops or message handling.Integrations replace dispatch functions or intercept request-issuance methods, forwarding actions to the reference monitor.
  • Implementation: FORGE registers action dependencies before verdict evaluation and synchronizes policy workers using monotonic graph-update sequence numbers.This ordering lets stateful policies evaluate the relevant execution history.
  • Conclusion: FORGE’s comparison identifies it as the only surveyed approach combining expressive policies, recursion, causal dependencies, multi-agent support, and deterministic enforcement.These five dimensions are the comparison criteria reported for the surveyed approaches.
  • Case study: The inter-agent privacy deployment combines semantic content checks with deterministic structural approval gates.Structural rules require a reachable VP approval signal, whereas semantic rules can evaluate response text and permit retries.

C.3 Security Properties and Limitations

The coding-agent deployment uses causal scan-coverage rules to block unsafe pushes and can force earlier scanning as uncovered changes accumulate. Its guarantees depend on trusted scanners and deployment-specific policy authoring.

  • Security properties: Every edit reaching a git push must be transitively covered by a passing security scan through the dependency graph.The policy requires gitleaks, dependency, and SAST coverage according to the edited content and the push’s backward slice.
  • Security properties: When uncovered edits exceed 1000 lines, further edit-like actions are blocked until a passing SAST scan covers them.The aggregate shifts scanning earlier without changing the full-coverage guarantee at the push boundary.

D.3 Security Properties and Limitations

The deployment defines causal coverage and scan integrity through structural policy rules that prevent pushes without appropriate passing scans. Its guarantees remain bounded by trusted scanner behavior and deployment-specific configuration.

  • Security properties: Every edit must be followed by a passing scan whose dependency path reaches the eventual push; scans run beforehand do not satisfy coverage.Coverage is defined by reachability in the dependency graph.
  • Security properties: Scan integrity comes from matching PASS in registered scanner results rather than relying on the agent’s judgment.The policy therefore checks the recorded tool output used by the enforcement system.
  • Security properties: Structural gates are unaffected by adversarial framing of edited content because they do not semantically inspect vulnerability content.Their decision depends on causal scan evidence and tool-result registration.
  • Limitations: The deployment trusts its security tools, so a false negative from an underlying scanner becomes a false negative for the policy.The 1000-line threshold is a demo heuristic, and the rules are authored for Copilot Chat’s tool surface.

E.1 System and Tasks

The case studies test FORGE against prompt injection, information-flow constraints, and organizational workflow policies across airline and retail tasks. FORGE blocks unauthorized actions while permitting compliant workflows, with structured feedback supporting recovery.

  • Prompt-injection defense: The prompt-injection scenario combines classified files, external email, and injected claims of executive authorization to induce sensitive-data exfiltration.The benign counterpart reads a SECRET report and emails an authorized internal recipient.
  • Information-flow enforcement: MLS blocks unauthorized reads or external sends according to clearance, while toxic-flow blocks external email after untrusted and sensitive data enter the context.Under MLS TOP_SECRET, all 9 external send attempts are blocked; toxic-flow blocks 6 external email attempts across 5 adversarial trials.
  • Prompt-injection defense: Without enforcement, GPT-4.1-mini follows the injection and sends top-secret merger plans to the attacker in all 5 trials.The baseline overrides the natural-language anti-exfiltration policy after accepting the injection's claimed authorization.
  • Runtime recovery: FORGE's structured denial feedback identifies tainted context and advises against external email, allowing the agent to halt or redirect rather than repeat the action.This feedback makes the policy violation actionable during runtime.
  • Organizational workflows: In airline and retail workflows, policies use Datalog rules over conversational context or prior tool results to constrain booking, cancellation, payment, and order operations.The airline policy has roughly forty rules spanning five concerns, while retail rules track state across orders and required lookups.
  • Organizational workflows: The dominant non-instrumented violation mode is adversarial reframing and persistent pressure, which FORGE blocks deterministically.Agents otherwise treat reframed requests as newly valid rather than preserving the underlying intent.

F.4 Per-RQ Detailed Analysis

The airline and retail evaluation measures compliance, task success, and overhead under runtime policy enforcement. Instrumentation substantially improves compliance while preserving most task success, with overhead driven mainly by corrective retries.

  • RQ1 (Compliance): Compliance improves from 58% (52/90) to 98% (88/90), with all three recurring violation modes blocked by Datalog rules.The rules analyze conversational context in airline tasks and an action's backward slice in retail tasks, with all true positives.
  • RQ2 (Task Success): Two failures across 90 instrumented trials are reasoning errors rather than policy violations.One follows failed recovery after a blocked cancellation; the other selects the wrong payment method, also observed without instrumentation.
  • RQ3 (Overhead): Instrumentation adds approximately 38% average latency in airline and 19% in retail, while token costs rise approximately 26% and 23%, respectively.Authorization decisions themselves contribute negligibly; corrective-feedback retry reasoning dominates overhead.
  • Scope: The telecom domain is omitted because its leaderboard performance exceeds a 98% best pass rate, leaving little policy-related compliance margin to evaluate.The reported evaluation therefore focuses on airline and retail domains with substantial natural-language constraints.

G.3 Per-RQ Detailed Analysis

The pharmacovigilance evaluation tests whether FORGE enforces approval workflows without harming scientific task accuracy. Runtime blocking eliminates unauthorized FDA access, and agents recover through repeated approval steps while incurring retry overhead.

  • RQ1 (Compliance): Instrumentation blocks all 40 unauthorized FDA API attempts across 15 non-instrumented trials and requires approval within each agent's current session.Prior approvals do not carry over when DrugAgent delegates to FDAHandler in a new execution session.
  • RQ1 (Compliance): All instrumented trials successfully complete the multi-step recovery pattern after the first registration attempt is rejected or requires waiting.The agent must call register_fda_usage again before retrying the FDA query.
  • RQ2 (Task Success): Instrumented trials achieve 15/15 correct predictions, matching the 15/15 non-instrumented baseline.The evaluation covers three pharmacovigilance questions with expected decrease, increase, or no-effect outcomes.
  • RQ3 (Overhead): Average trial time rises from 72.5 seconds to 95.4 seconds, while cost increases from $0.072 to $0.103 per trial.The additional latency and cost come from denial feedback, approval calls, and retried FDA queries.
  • Runtime recovery: FORGE's denial feedback names the blocked endpoint, identifies the missing authorization, and instructs the agent to repeat registration until approval is obtained.This makes the recovery procedure explicit rather than leaving the agent to infer why the request failed.
Loading 2602.16708v3…